yusuke1997/dblp-id-title huggingface dataset:
System Description: DLP
Anti-pattern Templates
Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings
Unification Modulo Lists with Reverse Relation with Certain Word Equations
Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics
Ordered Resolution vs. Connection Graph Resolution
System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning
Certifying Solutions to Permutation Group Problems
Regular Protocols and Attacks with Regular Knowledge
Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover
Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
Superposition Modulo a Shostak Theory
A Case for Query-driven Predicate Answer Set Programming
Barendregt's Variable Convention in Rule Inductions
Monodic Temporal Resolution
Challenge Equality Problems in Lattice Theory
Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers
Automation of Formal Verification of PLC Programs Written in IL
Theorem Proving in Non-Standard Logics Based on the Inverse Method
An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQ
A Narrowing Procedure for Theories with Constructors
System Description: SPASS-FD
AC Completion with Termination Tools
Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi
Type Inference in Prolog
The Next W ALDMEISTER Loop
Labelled Calculi for Quantified Modal Logics with Non-rigid and Non-denoting Terms
Multi-Dimensional Interpretations for Termination of Term Rewriting
A Geometry Theorem Prover Based on Buchberger's Algorithm
Machine Learner for Automated Reasoning 0.4 and 0.5
Solving Systems of Linear Inequalities by Bound Propagation
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae
Proving Equality Theorems with Hyper-Linking
LEO-II Version 1.5
Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory
Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics
Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic
Strict Basic Superposition
Optimal Axiomatizations for Multiple-Valued Operators and Quantifiers Based on Semi-lattices
The QED Manifesto
Exploiting Symmetry in SMT Problems
Leśniewski's Ontology - Proof-Theoretic Characterization
A Connection-Based Characterization of Bi-intuitionistic Validity
A Decision Procedure for Restricted Intensional Sets
Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings
Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols
A New Method for Knowledge Compilation: The Achievement by Cycle Search
An Efficient Decision Procedure for Imperative Tree Data Structures
The eXtended Least Number Heuristic
Rewrite Semantics for Production Rule Systems: Theory and Applications
Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract)
Dei: A Theorem Prover for Terms with Integer Exponents
Interpolation and Symbol Elimination
Fast Cube Tests for LIA Constraint Solving
Static Analysis of Android Programs
Splitting Proofs for Interpolation
Lazy Theorem Proving for Bounded Model Checking over Infinite Domains
Conflicts, Models and Heuristics for Quantifier Instantiation in SMT
KK: a theorem prover for K
Certified Size-Change Termination
The Design of the CADE-13 ATP System Competition
Quantifier Instantiation Techniques for Finite Model Finding in SMT
Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, Sydney, Australia, August 10-11, 2008
The 2012 SMT Competition
BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics
The Crisis in Finite Mathematics: Automated Reasoning as Cause and Cure
Workshop on Evaluation Methods for Solvers, and Quality Metrics for Solutions, EMSQMS 2010, Edinburgh, UK, July 20, 2010
A Resolution-Based Decision Procedure for SHOIQ
Minlog: A Minimal Logic Theorem Prover
On the Saturation of YAGO
Regression Tests and the Inventor's Dilemma
leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
Str+ve and Integers
SETHEO V3.2: Recent Developments - System Abstract
Deductive Search for Errors in Free Data Type Specifications Using Model Generation
Deciding Simple Infinity Axiom Sets with One Binary Relation by Means of Superpostulates
Hierarchical Combination
AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description
Reasoning about Qualitative Representations of Space and Time
Automatically Building Diagrams for Olympiad Geometry Problems
A Computational Logic Approach to Syllogisms in Human Reasoning
An Infrastructure for Intertheory Reasoning
Unification in Lambda-Calculi with if-then-else
Generalisation of Induction Formulae based on Proving by Symbolic Execution
Expressing Symmetry Breaking in DRAT Proofs
Parallel Algorithms for Term Matching
Unified Classical Logic Completeness - A Coinductive Pearl
The Tableau-Based Theorem Prover 3 T A P for Multi-Valued Logics
Exploring Approximations for Floating-Point Arithmetic Using UppSAT
Superposition for Full Higher-order Logic
Synthesis for Unbounded Bit-Vector Arithmetic
MUltlog 1.0: Towards an Expert System for Many-Valued Logics
Focusing in Linear Meta-logic
Neural Precedence Recommender
SGGS Decision Procedures
Hierarchic Reasoning in Local Theory Extensions
Confluence Criteria for Logically Constrained Rewrite Systems
Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices
Implementation Strategies for Plan-Based Deduction
Reachability Analysis of Program Variables
Decision Problems in a Logic for Reasoning About Reconfigurable Distributed Systems
Algebraic Factoring and Geometry Proving
Fair Derivations in Monodic Temporal Reasoning
A Mechanization of Strong Kleene Logic for Partial Functions
An Embedding of Ruby in Isabelle
Free Sequentially in Orthogonal Order-Sorted Rewriting Systems with Constructors
A Note on Symmetry Heuristics in SEM
Controlling Deduction with Proof Condensation and Heuristics
Decreasing Diagrams and Relative Termination
Verified Path Indexing
Beagle as a HOL4 external ATP method
Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity
The Special-Relation Rules are Incomplete
Reflection of Formal Tactics in a Deductive Reflection Framework
Interpolation in Local Theory Extensions
Diamond Formulas in the Dynamic Logic of Recursively Enumerable Programs
Towards Fast Nominal Anti-unification of Letrec-Expressions
How to Prove Algebraic Inductive Hypotheses Without Induction
TaMeD: A Tableau Method for Deduction Modulo
Representing Infinite Sequences of Resolvents in recursive First-Order Horn Databases
Computational Aspects of Three-Valued Logic
Canonical Propositional Gentzen-Type Systems
Isabelle-91
Canonical Inference for Implicational Systems
Ordered Resolution with Straight Dismatching Constraints
New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants
Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings
The Semantically Guided Linear Deduction System
Escape to Mizar from ATPs
Tackling Benchmark Problems of Commonsense Reasoning
Abstractions Before Proofs
Unification Algorithms Cannot be Combined in Polynomial Time
Knowledge Retrieval as Limited Inference
Bunched Logic Programming
A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description
Preferred Extensions of Argumentation Frameworks: Query Answering and Computation
User-friendly Support for Common Mathematical Concepts in a Lightweight Verifier
Behind the Scene of Solvers Competitions: the "evaluation" Experience
Support Ordered Resolution
Equality Preprocessing in Connection Calculi
Stumbling Around in the Dark: Lessons from Everyday Mathematics
Efficient Verified (UN)SAT Certificate Checking
UEL: Unification Solver for the Description Logic ℇℒ - System Description
A Simple Semi-automated Proof Assistant for First-order Modal Logics
Solving Open Questions with an Automated Theorem-Proving Program
Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings
On the Complexity of Equational Horn Clauses
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness
Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time
BDD-based automated reasoning in propositional non-classical logics: progress report
Give Reasoning a Trie
Automated Reasoning for Relational Probabilistic Knowledge Representation
Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings
System Description: RDL : Rewrite and Decision Procedure Laboratory
A Colored Version of the Lambda-Calculus
LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
Lash 1.0 (System Description)
Tree Automata with Equality Constraints Modulo Equational Theories
Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning
Proving Simpson's Four-Slot Algorithm Using Ownership Transfer
Semantic Tableaux with Ordering Restrictions
CODE: A Powerful Prover for Problems of Condensed Detachment
VSDITLU: a verifiable symbolic definite integral table look-up
GEO-Prover - A Geometry Theorem Prover Developed at UT
A Combinator-Based Superposition Calculus for Higher-Order Logic
Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems
Commutation, Transformation, and Termination
Some Tools for an Inference Laboratory (ATINF)
Term Rewriting Induction
Fingerprint Indexing for Paramodulation and Rewriting
Privacy-Sensitive Information Flow with JML
Proof Script Pragmatics in IMPS
Complexity of Fractran and Productivity
Equational Reasoning Modulo Commutativity in Languages with Binders
The Tableau-based Theorem Prover 3 T A P Version 4.0
A Tableaux Calculus for Reducing Proof Size
A dynamic programming approach to categorial deduction
Term Rewriting Systems and Algebra
CheAPS: a Checker of Asynchronous Parameterized Systems
Presburger Modal Logic Is PSPACE-Complete
6th Conference on Automated Deduction, New York, USA, June 7-9, 1982, Proceedings
Reducing Relative Termination to Dependency Pair Problems
Modal Theorem Proving
Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments
Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings
RALL: Machine-Supported Proofs for Relation Algebra
KITP-93: An Automated Inference System for Program Analysis
Finite Quantification in Hierarchic Theorem Proving
Building Theorem Provers
Kneecap: Model-based Generation of Network Traffic
Program Synthesis from Incomplete Specifiactions
Analogical Reasoning and Proof Discovery
Sort It Out with Monotonicity - Translating between Many-Sorted and Unsorted First-Order Logic
Specification and Verification of Real-Time, Distributed Systems Using the Theory of Constraints
Stratification in Logics of Definitions
Internal Guidance for Satallax
Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
On Intervals and Bounds in Bit-vector Arithmetic
Towards Physical Hybrid Systems
A Science of Reasoning: Extended Abstract
Proving Termination and Memory Safety for Programs with Pointer Arithmetic
Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
A Dynamic Logic for Configuration
Semantic Relevance
An Examination of the Prolog Technology Theorem-Prover
MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction
System Description: card T A P : The First Theorem Prover on a Smart Card
Combination of Disjoint Theories: Beyond Decidability
About the Confluence of Equational Pattern Rewrite Systems
Reasoning with Expressive Description Logics: Theory and Practice
Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers
CTL * Model Checking for Data-Aware Dynamic Systems with Arithmetic
On Checking Kripke Models for Modal Logic K
Multi-completion with Termination Tools (System Description)
Generating Contours of Integration: An Application of Prolog in Symbolic Computing
On the Width of Regular Classes of Finite Structures
XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description
A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems
Rewrite Systems for Varieties of Semigroups
Counting Constraints in Flat Array Fragments
Canonical Conditional Rewrite Systems
Associative-Commutative Unification
The Fractal Dimension of SAT Formulas
Automation for Geometry in Isabelle/HOL
A Resolution Principle for Clauses with Constraints
Hybrid Interactive Theorem Proving Using Nuprl and HOL
qbf2epr: A Tool for Generating EPR Formulas from QBF
Politeness and Stable Infiniteness: Stronger Together
A New Probabilistic Algorithm for Approximate Model Counting
The Matita Interactive Theorem Prover
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
Automatically Proving and Disproving Feasibility Conditions
The Uses of SAT Solvers in Vampire
Solving Constraints by Elimination Methods
Confluence Competition 2015
Automatic generation of high quality test sets via CBMC
Reasoning with Triggers
AUTOLOGIC at University of Victoria
Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems
A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions
On Word Problems in Horn Theories
A Model-Based Completeness Proof of Extended Narrowing and Resolution
The Complexity of Conjunctive Query Answering in Expressive Description Logics
Termination of Algorithms over Non-freely Generated Data Types
Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings
Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning, Sydney, Australia, August 10-11, 2008
Connection Tableaux with Lazy Paramodulation
Compression of Propositional Resolution Proofs via Partial Regularization
Invited Talk: Rewrite-based Deduction and Symbolic Constraints
System Description: H-PILoT
Model Representation via Contexts and Implicit Generalizations
Matrix Interpretations for Proving Termination of Term Rewriting
Recent Advances in Unification for the EL Family
Ground Interpolation for Combined Theories
A Satisfiability Tester for Non-Clausal Propositional Calculus
Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings
Proof Search with Set Variable Instantiation in the Calculus of Constructions
Induction in Saturation-Based Proof Search
On Shostak's Decision Procedure for Combinations of Theories
Propositional Temporal Interval Logic is PSPACE Complete
The Central Variable Strategy of Str+ve
Uniform Substitution for Differential Game Logic
Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
Unification in Finite Algebras is Unitary (?)
GRUNGE: A Grand Unified ATP Challenge
Combined Covers and Beth Definability
Algorithms for Ordinal Arithmetic
The CoRe Calculus
Optimization Modulo the Theory of Floating-Point Numbers
Similarity-based Relaxed Instance Queries in EL++
KoMeT
Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+
Using the TPTP Language for Writing Derivations and Finite Interpretations
Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor
A Proof Environment for the Development of Group Communication Systems
Presenting Intuitive Deductions via Symmetric Simplification
Formal Device and Programming Model for a Serial Interface
A Gentle Non-disjoint Combination of Satisfiability Procedures
Fast Decision Procedure for Propositional Dummett Logic Based on a Multiple Premise Tableau Calculus
System Demonstration: The Higher-Order Prover Leo-III
Subsumption Demodulation in First-Order Theorem Proving
Selective Backtracking for Logic Programs
System Description: IVY
XBarnacle: Making Theorem Provers More Accessible
The KIV System: Systematic Construction of Verified Software
Deciding the First-Order Theory of an Algebra of Feature Trees with Updates
5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings
On Intuitionistic Query Answering in Description Bases
Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings
Designing a solver competition: the QBFEVAL'10 case study
A Small Framework for Proof Checking
The Imandra Automated Reasoning System (System Description)
Full-Commutation and Fair-Termination in Equational (and Combined) Term-Rewriting Systems
Experiments on Supporting Interactive Proof Using Resolution
Congruence Closure in Intensional Type Theory
A Commonsense Theory of Nonmonotonic Reasoning
Verifying Mixed Real-Integer Quantifier Elimination
Formalizing the Face Lattice of Polyhedra
A Resolution Decision Procedure for the Guarded Fragment
Does This Set of Clauses Overlap with at Least One MUS?
KRHyper - In Your Pocket
Program Verification as Satisfiability Modulo Theories
Two Automated Methods in Implementation Proofs
Program Synthesis in Saturation
The Clause-Diffusion Theorem Prover Peers-mcd (System Description)
mu-term: Verify Termination Properties Automatically (System Description)
Beyond Dependency Graphs
Quantifier-Free Equational Logic and Prime Implicate Generation
Variable Elimination and Chaining in a Resolution-based Prover for Inequalities
Premise Selection in the Naproche System
DPLL-based Procedure for Equality Logic with Uninterpreted Functions
Proof Search in the Intuitionistic Sequent Calculus
Proceedings of the First Workshop on Logics for Reasoning about Preferences, Uncertainty, and Vagueness, PRUV 2014, co-located with 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Vienna, Austria, July 23-24, 2014
Source-Tracking Unification
The Oyster-Clam System
Intelligent Theorem Proving for Specific Domains
Reasoning About Loops Using Vampire
Advancing Automated Theorem Proving for the Modal Logics D and S5
SCL(EQ): SCL for First-Order Logic with Equality
Proving Termination of Programs Automatically with AProVE
Skeptik: A Proof Compression System
Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays
Model Checking Parameterised Multi-token Systems via the Composition Method
From Syntactic Proofs to Combinatorial Proofs
Things You Can't do With a Vampire
Minimizing the Number of Clauses by Renaming
dReal: An SMT Solver for Nonlinear Theories over the Reals
KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS
Incremental Closure of Free Variable Tableaux
Superposition and Model Evolution Combined
Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions
Proof Search Optimizations for Non-Clausal Connection Calculi
Efficient E-Matching for SMT Solvers
Practical Proof Search for Coq by Type Inhabitation
Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4
Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic
Infinite State Model Checking by Learning Transitive Relations
Combining Theorem Proving with Natural Language Processing
Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs
Integration of Automated and Interactive Theorem Proving in ILP
Automated Verification of Recursive Programs with Pointers
Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny
The Anatomy of Equinox - An Extensible Automated Reasoning Tool for First-Order Logic and Beyond - (Talk Abstract)
Theory Exploration: a role for Model Theory?
Local Reductions for the Modal Cube
Verification of Security Protocols
A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic
Procedure Implementation Through Demodulation and Related Tricks
System Description: MBASE, an Open Mathematical Knowledge Base
On the Organisation of Program Verification Competitions
System Description: ARA - An Automatic Theorem Prover for Relation Algebras
Abstraction Using Generalization Functions
A Decision Procedure for String to Code Point Conversion
Politeness for the Theory of Algebraic Datatypes
MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
Programming with Equations: A Framework for Lazy Parallel Evaluation
A Powerful Technique to Eliminate Isomorphism in Finite Model Search
Problems on the Generation of Finite Models
On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices
Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
Tractable Transformations from Modal Provability Logics into First-Order Logic
RCL: A Lisp Verification System
Plagiator - A Learning Prover
FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics
Reachability Modulo Theory Library
Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language
An Abstract Machine for Fixed-Order Dynamically Stratified Programs
A Unified Proof System for QBF Preprocessing
Efficient Encodings of First-Order Horn Formulas in Equational Logic
System Description: *SAT: A Platform for the Development of Modal Decision Procedures
The Application of Homogenization to Simultaneous Equations
Computing Tropical Prevarieties With Satisfiability Modulo Theories (SMT) Solvers
The TPS Theorem Proving System
A Completion-Based Method for Mixed Universal and Rigid E-Unification
Certified Equational Reasoning via Ordered Completion
ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017
Shostak Light
Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains: Extended Abstract
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
Adding Equivalence Classes to Stalmarck's Method in First Order Logic
Automated Implicit Computational Complexity Analysis (System Description)
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers
Counter-Model Search in Gödel-Dummett Logics
System Description: GCLCprover + GeoThms
Satallax: An Automatic Higher-Order Prover
Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic
iProver-Eq: An Instantiation-Based Theorem Prover with Equality
Towards Automated Property Discovery within Hume
Leveraging Probabilistic Existential Rules for Adversarial Deduplication
Lemma Discovery in Automated Induction
Rank/Activity: A Canonical Form for Binary Resolution
Solving Disequations in Equational Theories
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms
FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions
What is a Proof? (Abstract)
Operating System Verification for Real Use
Ground Resolution with Group Computations on Semantic Symmetries
Solving Sparse Linear Constraints
Analysing Vote Counting Algorithms via Logic - And Its Application to the CADE Election Scheme
Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure
Caching and Lemmaizing in Model Elimination Theorem Provers
leanT A P: Lean Tableau-Based Theorem Proving (Extended Abstract)
A Top-Down Procedure for Disjunctive Well-Founded Semantics
Unification Modulo ACU I Plus Homomorphisms/Distributivity
δ-Complete Decision Procedures for Satisfiability over the Reals
Using f-SHIN to Represent Objects: An Aid to Visual Grasping
Foundational Proof Certificates in First-Order Logic