yusuke1997/dblp-id-title huggingface dataset:
The Problem of Induction
Theorem Proving for Intensional Logic
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry
An Algorithm for Dual Transformation in First-Order Logic
POSIX Lexing with Derivatives of Regular Expressions
Set Theory in First-Order Logic: Clauses for Gödel's Axioms
What Is Automated Theorem Proving?
Hierarchical Deduction
Inference Flexibility in Horn Clause Knowledge Bases and the Simplex Method
Induction Using Term Orders
Reasoning about Qualitative Spatial Relationships
leanTAP: Lean Tableau-based Deduction
On subsumption in distributed derivations
A Branching Time Temporal Framework for Quantitative Reasoning
Mechanized Semantics for the Clight Subset of the C Language
A Decision Method for Nonmonotonic Reasoning Based on Autoepistemic Reasoning
Simulating Circuit-Level Simplifications on CNF
The Procedures of the CADE-13 ATP System Competition
The Problem of Finding a Semantic Strategy for Focusing Inference Rules
A Synthetic Proof of Pappus' Theorem in Tarski's Geometry
The Disconnection Tableau Calculus
Formalization of Ring Theory in PVS
Signed Systems for Paraconsistent Reasoning
Preface to the Special Issue on Commonsense and Nonmonotonic Reasoning
Formally Verified Suffix Array Construction
Exploitation of Parallel Processing for Implementing High-Performance Deduction Systems
Investigations into Proof Structures
Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent Interleavings
Automated Proofs of Block Cipher Modes of Operation
Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers
A Superposition Calculus for Abductive Reasoning
Formalization of Euler-Lagrange Equation Set Based on Variational Calculus in HOL Light
A Family of Goal Directed Theorem Provers Based on Conjunction and Implication: Part I
The Problem of Definition Expansion and Contraction
A Sequent-Style Model Elimination Strategy and a Positive Refinement
A Mechanically Verified Language Implementation
What Is the Inverse Method?
Formalization of Convergence Rates of Four First-order Algorithms for Convex Optimization
The Problem of Demodulating Across Argument and Literal Boundaries
An Algorithm for General Set Unification and Its Complexity
Automated Generation of Readable Proofs with Geometric Invariants I. Multiple and Shortest Proof Generation
Towards Mechanical Metamathematics
Simplification in a Satisfiability Checker for VLSI Applications
Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory
A Formal Logic Approach to Constrained Combinatorial Testing
Preface to the Special Issue on Linearity
Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm
A Family of Dynamic Description Logics for Representing and Reasoning About Actions
The Use of Embeddings to Provide a Clean Separation of Term and Annotation for Higher Order Rippling
An Integrated Approach to High Integrity Software Verification
Single Elementary Associative-Commutative Matching
A Formalization of Powerlist Algebra in ACL2
Uncurrying for Termination and Complexity
Challenge Problems in Elementary Calculus
MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers
"Handbook of Practical Logic and Automated Reasoning, " by John R. Harrison, Cambridge University Press, 2009
Subgoal Strategies for Solving Board Puzzles
Completeness of a Bytecode Verifier and a Certifying Java-to-JVM Compiler
Tractability Through Symmetries in Propositional Calculus
Emptiness and Finiteness for Tree Automata with Global Reflexive Disequality Constraints
An Optimal Decision Procedure for Right Propositional Neighborhood Logic
Four Decades of Mizar - Foreword
A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data
Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation
Alternative Translation Techniques for Propositional and First-Order Modal Logics
The 2013 Evaluation of SMT-COMP and SMT-LIB
A List-Machine Benchmark for Mechanized Metatheory
Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System
Limited Second-Order Functionality in a First-Order Setting
TMPR: A Tree-Structured Modified Problem Reduction Proof Procedure and Its Extension to Three - Valued Logic
Reasoning About Algebraic Data Types with Abstractions
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version
Writing Programs that Construct Proofs
Completeness of a Prover for Dense Linear Orders
The MetaCoq Project
Some Experiments in Nonassociative Ring Theory with an Automated Theorem Prover
Mechanisation of the AKS Algorithm
From Bisimulation to Simulation: Coarsest Partition Problems
Abstract Congruence Closure
Satisfiability in the Year 2005
CoCon: A Conference Management System with Formally Verified Document Confidentiality
A Graphical User Interface for Formal Proofs in Geometry
Solution of the Robbins Problem
Predicate Logic Hacker Tricks
A Formalization of SQL with Nulls
Higher-Order Pattern Anti-Unification in Linear Time
Proof-Guided Test Selection from First-Order Specifications with Equality
Transcendental Functions and Mechanical Theorem Proving in Elemantary Geometries
An Approximation Framework for Solvers and Decision Procedures
IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale
Semantics of Mizar as an Isabelle Object Logic
On the Fine-Structure of Regular Algebra
Meta-Level Inference: Two Applications
Enabling Floating-Point Arithmetic in the Coq Proof Assistant
Windmills of the Minds: A Hopping Algorithm for Fermat's Two Squares Theorem
Heuristic-Based Backtracking Relaxation for Propositional Satisfiability
The Strategy of Cramming
A Set-Theoretic Translation Method for Polymodal Logics
Tests and Proofs - Preface of the Special Issue
The Notion of Proof in Hardware Verification
Set Theory for Verification. II: Induction and Recursion
A Framework for the Verification of Certifying Computations
A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures
Conclusions about the CADE-13 ATP System Competition
ROGET: A Knowledge-Based System for Acquiring the Conceptual Structure of a Diagnostic Expert System
Proving Geometry Theorems with Rewrite Rules
Formally-Verified Round-Off Error Analysis of Runge-Kutta Methods
Evaluation of Queries under Closed-World Assumption. Part II: The Hierarchical Case
Andrzej Trybulec - in Memoriam
An Effective Algorithm for the Futile Questioning Problem
A Conflict-Driven Solving Procedure for Poly-Power Constraints
The Watson Theorem Prover
Complexity of Unification Problems with Associative-Commutative Operators
Human-Centered Automated Proof Search
Proving Self-Utterances
Balancing the Load
Schematic Program Proofs with Abstract Execution
The Problem of Automated Theorem Finding
SAT-Based Decision Procedures for Classical Modal Logics
Preface: Special Issue of Selected Extended Papers from IJCAR 2018
ATP and Presentation Service for Mizar Formalizations
Politeness and Combination Methods for Theories with Bridging Functions
How to Avoid the Derivation of Redundant Clauses in Reasoning Systems
Certification of a Type Inference Tool for ML: Damas-Milner within Coq
Learning-Assisted Automated Reasoning with Flyspeck
Mechanical Theorem Proving of Differential Geometries and Some of its Applications in Mechanics
Autoepistemic Circumscription and Logic Programming
Triviality and Dimension of a System of Algebraic Differential Equations
A Formal Theory of Choreographic Programming
Partial Functions in a Total Setting
On the Formalization of Gamma Function in HOL
CNF and DNF Considered Harmful for Computing Prime Implicants/Implicates
Some Computational Aspects of distance-sat
The Problem of Choosing between Predicate and Function Notation for Problem Representation
The Incredible ELK - From Polynomial Procedures to Efficient Reasoning with ℰℒ Ontologies
Semi-intelligible Isar Proofs from Machine-Generated Proofs
Toward Automating the Discovery of Decreasing Measures
Finding Proofs in Tarskian Geometry
On the Completeness of SLDENF-Resolution
A New Approach for Automatic Theorem Proving in Real Geometry
A Library for Formalization of Linear Error-Correcting Codes
Implicit Induction in Conditional Theories
Preface: Selected Extended Papers of CADE 2017
An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model
The SAT-based Approach to Separation Logic
Visually Dynamic Presentation of Proofs in Plane Geometry - Part 2. Automated Generation of Visually Dynamic Presentations with the Full-Angle Method and the Deductive Database Method
A Formalization of the Smith Normal Form in Higher-Order Logic
A Verified Implementation of Algebraic Numbers in Isabelle/HOL
Preface to the Special Issue on Automated Reasoning Systems
A Full Formalization of SLD-Resolution in the Calculus of Inductive Constructions
SETHEO and E-SETHEO - The CADE-13 Systems
Complete Instantiation-Based Interpolation
Structured Theory Development for a Mechanized Logic
Living Book - Deduction, Slicing, and Interaction
Relative Security: (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities in Isabelle/HOL
A Formalized General Theory of Syntax with Bindings: Extended Version
New Uses of Linear Arithmetic in Automated Theorem Proving by Induction
Things to Know when Implementing KBO
Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005)
User Interaction with the Matita Proof Assistant
SLDNF-Resolution with Equality
Bytecode Verification by Model Checking
PSPACE Tableau Algorithms for Acyclic Modalized $\boldsymbol{\mathcal{ALC}}$
Compiling Bottom-up and Mixed Derivations into Top-down Executable Logic Programs
Generalizing Morley's and Other Theorems with Automated Realization
Proving Consistency Assertions for Automotive Product Data Management
Using Isabelle/HOL to Verify First-Order Relativity Theory
A Note on Assumptions about Skolem Functions
Certified Quantum Computation in Isabelle/HOL
A Benchmark Method for the Propositional Modal Logics K, KT, S4
Preface: Special Issue on Uncertain Reasoning
Inferring from Inconsistency in Preference-Based Argumentation Frameworks
Discovering Inequality Conditions in the Analytic Solution of Optimization Problems
The Complexity of Pure Literal Elimination
Editorial: A Journal Is Born
Robbins Algebra: Conditions That Make a Near-Boolean Algebra Boolean
Automated Deduction in von Neumann-Bernays-Gödel Set Theory
On the Generation of Quantified Lemmas
A New Technique for Verifying and Correcting Logic Programs
An Alternative Approach to the Semantics of Disjunctive Logic Programs and Deductive Databases
Some Techniques for Proving Termination of the Hyperresolution Calculus
A Milestone Reached and a Secret Revealed
A Hyperbase for Binary Lattice Hyperidentities
Resolution versus Search: Two Strategies for SAT
Experiences from Exporting Major Proof Assistant Libraries
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
Backchain Iteration: Towards a Practical Inference Method That Is Simple Enough to Be Proved Terminating, Sound, and Complete
The CADE-14 ATP System Competition
Paramodulation with Non-Monotonic Orderings and Simplification
An Efficient Algorithm to Generate Prime Implicants
A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties
The Higher-Order Prover Leo-II
The Semantics of Answer Literals
The Anatomy of Vampire Implementing Bottom-up Procedures with Code Trees
Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions
Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic
The Results - of the CADE-13 ATP System Competition
More on the Problem of Finding a Mapping between Clause Representation and Natural Deduction Representation
A Tableaux Prover for Domain Minimization
Double Auctions: Formalization and Automated Checkers
Computing Circumscription Revisited: A Reduction Algorithm
Formalization of Definitions and Theorems Related to an Elliptic Curve Over a Finite Prime Field by Using Mizar
A Technical Note on AC-Unification. The Number of Minimal Unifiers of the Equation alpha x 1 + . . . + alpha x p = AC beta y 1 + . . . + beta y q
Non-termination in Term Rewriting and Logic Programming
The CADE-17 ATP System Competition
Searching for Circles of Pure Proofs
Reasoning Theories
Tableaux and Sequent Calculus for Minimal Entailment
Analyzing Read-Once Cutting Plane Proofs in Horn Systems
Fast Left Kan Extensions Using the Chase
Eliciting Implicit Assumptions of Mizar Proofs by Property Omission
On the Role of Automated Theorem Proving in the Compile-Time Derivation of Concurrency
SPASS - Version 0.49
A Mechanical Analysis of Program Verification Strategies
Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover
Relevant Logic Programming
The Heine-Borel Challenge Problem. In Honor of Woody Bledsoe
Towards Satisfiability Modulo Parametric Bit-vectors
A Fully Automatic Theorem Prover with Human-Style Output
Satisfiability in the Year 2000
Model Elimination Without Contrapositives and Its Application to PTTP
Formalization of the Computational Theory of a Turing Complete Functional Language Model
Theorem Proving Based on the Extension Rule
A New Implementation of Automath
Proof Pearl - A Mechanized Proof of GHC's Mergesort
Resolution for Skeptical Stable Model Semantics
Evaluation of Queries under Closed-World Assumption
Measuring the Readability of Geometric Proofs: The Area Method Case
CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics
Verifying the Generalization of Deep Learning to Out-of-Distribution Domains
Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs
Terminating Calculi for Propositional Dummett Logic with Subformula Property
Implementing and Reasoning About Hash-consed Data Structures in Coq
MizAR 40 for Mizar 40
Fuzzy Operator Logic and Fuzzy Resolution
A Complete Superposition Calculus for Primal Grammars
On Interpolation in Automated Theorem Proving
The TPTP Problem Library - CNF Release v1.2.1
A Mechanization of Unity in PC-NQTHM-92
Preface: Selected Extended Papers of CADE 2015
Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation
Theorem of Three Circles in Coq
Relative Termination via Dependency Pairs
The Problem of Choosing the Type of Subsumption to Use
Selected Extended Papers of ITP 2017 - Preface
Automated reasoning for proving non-orderability of groups
Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL
On the Declarative and Procedural Semantics of Logic Programs
Correction to: Local is Best: Efficient Reductions to Modal Logic K
OTTER and the Moufang Identity Problem
A Matrix Characterization for Multiplicative Exponential Linear Logic
A Resolution Proof System for Dependency Stochastic Boolean Satisfiability
Proof Pearl: Regular Expression Equivalence and Relation Algebra
The Inevitability of Inconsistent Abstract Spaces
Visualizing SAT Instances and Runs of the DPLL Algorithm
Studies of a Theory of Specifications with Built-in Program Extraction
Constraint Solving for Proof Planning
Modular & Incremental Automated Termination Proofs
On the Computation of the Disjunctive Well-Founded Semantics
Decision Procedures for Elementary Sublanguages of Set Theory
The Problem of Finding an Inference Rule for Set Theory
A Presheaf Environment for the Explicit Fusion Calculus
"Decision Procedures: An Algorithmic Point of View, " by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008
Mechanical Certification of Systolic Algorithms
Tuple Interpretations for Termination of Term Rewriting
On Process Equivalence = Equation Solving in CCS
Meteor: Exploring Model Elimination Theorem Proving
Termination of Floating-Point Computations
Selected and Extended Papers from TACAS 2018: Preface
The Problem of Finding a Strategy to Control Binary Paramodulation
The Ackermann Constant Theorem: A Computer-Assisted Investigation
The Problem of Guaranteeing the Existence of a Complete Set of Reductions
Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations
Correction to: A Unifying View on SMT-Based Software Verification
A Note on the Parallel Complexity of Anti-Unification
'Classical' Negation in Nonmonotonic Reasoning and Logic Programming
Formal Models and Analysis of Secure Multicast in Wired and Wireless Networks
Research in Intelligent Robots
Hammer for Coq: Automation for Dependent Type Theory
A Practical Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted Quantifiers
Non-Negative Integer Basis Algorithms for Linear Equations with Integer Coefficients
Preface: Theory and Applications of Abstraction, Substitution and Naming
Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL
Formal Mathematics for Mathematicians - Foreward to the Special Issue
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts
Set of Support, Demodulation, Paramodulation: A Historical Perspective
A Proof of GMP Square Root
Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints
Hybrid - A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax
An Introduction to Wu's Method for Mechanical Theorem Proving in Geometry
Deduction Trees and the View Update Problem in Indefinite Deductive Databases
Distributivity in [Lstrok][aleph]0 and Other Sentential Logics
Anti-unification for Unranked Terms and Hedges
Some Group Theoretic Examples with Completion Theorem Provers
Measure Construction by Extension in Dependent Type Theory with Application to Integration
Set Graphs. III. Proof Pearl: Claw-Free Graphs Mirrored into Transitive Hereditarily Finite Sets
Crystal: Integrating Structured Queries into a Tactic Language
More Proofs of an Axiom of Lukasiewicz
Generalization in the Presence of Free Variables: A Mechanically-Checked Correctness Proof for one Algorithm
Formal Power Series
Selected Extended Papers of ITP 2016: Preface
Formalization of the Prime Number Theorem with a Remainder Term
Mechanizing Metatheory Without Typing Contexts
Handling Transitive Relations in First-Order Automated Reasoning
SLT-Resolution for the Well-Founded Semantics
Symbolic Techniques in Satisfiability Solving
Finding Normal Binary Floating-Point Factors Efficiently
Nonstandard Analysis in ACL2
Proof Pearl: a Formal Proof of Higman's Lemma in ACL2
Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing
Lightweight Bytecode Verification
An Instantiation Scheme for Satisfiability Modulo Theories
Automated Reasoning and Nonclassical Logics: Introduction
Interpreting Disjunctive Logic Programs Based on a Strong Sense of Disjunction
A Mechanically Verified Garbage Collector for OCaml
Finding Shortest Proofs: An Application of Linked Inference Rules
Tableaux-Based Characterization and Theorem Proving for default Logic
Formally Verifying the Solution to the Boolean Pythagorean Triples Problem
Stable and Extension Class Theory for Logic Programs and Default Logics
Third Special Issue on Techniques for Automated Termination Proofs
Canonicity for Cubical Type Theory
A Mechanized Proof of the Basic Perturbation Lemma
The Problem of Self-Analytically Choosing the Weights
Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra
Link Inheritance in Abstract Clause Graphs
Pardinus: A Temporal Relational Model Finder
Preference Fusion for Default Reasoning Beyond System Z
Cotrolled Integration of the Cut Rule into Connection Tableaux Calculi
Mechanical Procedure for Proof Construction via Closed Terms in Typed \lambda Calculus
A Framework for Automated Reasoning in Multiple-Valued Logics
Formalization of the Poincaré Disc Model of Hyperbolic Geometry
Data Compression for Proof Replay
Partial and Nested Recursive Function Definitions in Higher-order Logic
Automated Discovery of Geometric Theorems Based on Vector Equations
Preface: Special Issue of Selected Extended Papers of IJCAR 2010
Automated Deduction Techniques for Classification in Description Logic Systems
Middle-Out Reasoning for Synthesis and Induction
Inferring Negative Information from Disjunctive Databases
A Note on a Canonical Theory with Undecidable Unification and Matching Problem
Model Theoretic Approach to View Updates in Deductive Databases
MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions
Superposition-based Equality Handling for Analytic Tableaux
Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL
General Algorithms for Permutations in Equational Inference
Call-by-Value Lambda Calculus as a Model of Computation in Coq
Constructing Finite Algebras with FALCON
Some Lambda Calculus and Type Theory Formalized
Formal Verification of a Generic Framework to Synthetize SAT-Provers
Short Single Axioms for Boolean Algebra
Exploring the Structure of an Algebra Text with Locales
Portfolios in Stochastic Local Search: Efficiently Computing Most Probable Explanations in Bayesian Networks
Special Issue on User Interfaces in Theorem Proving: Preface
Relational Program Reasoning Using Compiler IR - Combining Static Verification and Dynamic Analysis
Mechanizing Set Theory
BC D L \boldsymbol {\cal BC\!D\!L}: Basic Constructive Description Logic
Adding Equality to Semantic Tableaux
Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols
A simple proof of correctness of folding the regular heptagon
Model Minimization - An Alternative to Circumscription
A Formalization and Proof Checker for Isabelle's Metalogic
On Definitions of Constants and Types in HOL
Vectorial Equations Solving for Mechanical Geometry Theorem Proving
A Semantic Framework for Proof Evidence
A Legacy Recalled and a Tradition Continued
From QBFs to MALL and Back via Focussing
Verification in the Classroom
The IJCAR ATP System Competition
Computations in Fragments of Intuitionistic Propositional Logic
Binary Codes that do not Preserve Primitivity
Formally Verified Tableau-Based Reasoners for a Description Logic
Predicting and Detecting Symmetries in FOL Finite Model Search
The Unnormalized Dempster's Rule of Combination: A New Justification from the Least Commitment Principle and Some Extensions
Correction to: Certified First-Order AC-Unification and Applications
Shortest Single Axioms for the Equivalential Calculus with CD and RCD
Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem
Termination Proofs for String Rewriting Systems via Inverse Match-Bounds
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program
Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler
Rewriting Conversions Implemented with Continuations
A New Methodology for Query Answering in Default Logics via Structure-Oriented Theorem Proving
Parameterized Model Checking on the TSO Weak Memory Model
Psi-Calculi in Isabelle
The Problem of Guaranteeing the Absence of a Complete Set of Reductions
A Logic for Reasoning with Inconsistency
Solving Open Questions and Other Challenge Problems Using Proof Sketches
Automated Reasoning with Restricted Intensional Sets
Strong Extension-Free Proof Systems
Unifying Splitting
On Explicit Substitution with Names
A Certified Proof of the Cartan Fixed Point Theorems
Nested Abstract Syntax in Coq
Computational Complexity of Simultaneous Elementary Matching Problems
Efficient Query Processing with Reduced Implicate Tries
Bounded-Overhead Caching for Definite-Clause Theorem Proving
An Extension of a Procedure to Prove Statements in Differential Geometry
A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler
Automated Theorem Proving in Euler Diagram Systems
Abstract Proof Checking: An Example Motivated by an Incompleteness Theorem
The CADE-16 ATP System Competition
Branching Rules for Satisfiability
A Formal Proof of Sylow's Theorem
Simulating Strong Practical Proof Systems with Extended Resolution
Evidence Algorithm and Inference Search in First-Order Logics
Empirically Successful Automated Reasoning: Applications Issue