yusuke1997/dblp-id-title huggingface dataset:
FINDER: Finite Domain Enumerator - System Description
Computing Prime Implicates Incrementally
SC-square: when Satisfiability Checking and Symbolic Computation join forces
Reflecting Proofs in First-Order Logic with Equality
Equational Abstractions
Evidence Extraction from Parameterised Boolean Equation Systems
Relationships Between Probabilistic Description and First-Order Logics
A Decidable Class of Nested Iterated Schemata
The CADE-19 ATP System Competition
Proof Planning for First-Order Temporal Logic
Branching Time? Pruning Time!
Title, Preface, Table of Contents
A Comprehensive Framework for Saturation Theorem Proving
System Description: MCS: Model-based Conjecture Searching
Invited Talk: Decision procedures for guarded logics
Description Logics with Concrete Domains and General Concept Inclusions Revisited
Learning Precedences from Simple Symbol Features
Second International Workshop on Invariant Generation, WING 2009, York, UK, March 29, 2009 and Third International Workshop on Invariant Generation, WING 2010, Edinburgh, UK, July 21, 2010
Binary Codes that Do Not Preserve Primitivity
EUODHILOS-II on Top of GNU Epoch
Theoretical Study of Symmetries in Propositional Calculus and Applications
InKreSAT: Modal Reasoning via Incremental Reduction to SAT
The AFFIRM Theorem Prover: Proof Forests and Management of Large Proofs
From Modal Sequent Calculi to Modal Resolution
The Markgraf Karl Refutation Procedure (MKRP)
Computing All Implied Equalities via SMT-Based Partition Refinement
Unfolding Boxes with Local Constraints
A Rewriting Strategy to Generate Prime Implicates in Equational Logic
Rewriting for Cryptographic Protocol Verification
Experiments in the Heuristic Use of Past Proof Experience
Discovering Specifications for Unknown Procedures - Work in Progress
HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)
Linear Modal Deductions
A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo
Automated Complexity Analysis Based on the Dependency Pair Method
System Description: The Proof Transformation System CERES
Non-clausal Connection-based Theorem Proving in Intuitionistic First-Order Logic
A Decision Procedure for CTL * Based on Tableaux and Automata
'Living Book': -'Deduction', 'Slicing', 'Interaction'
Geometric Resolution: A Proof Procedure Based on Finite Model Search
raSAT: An SMT Solver for Polynomial Constraints
Efficient Minimal Model Generation Using Branching Lemmas
TRP++2.0: A Temporal Resolution Prover
Programming by Examples: Applications, Algorithms, and Ambiguity Resolution
Theory and Practice of Minimal Modular Higher-Order E-Unification
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description)
Automatic Acquisition of Search Guiding Heuristics
NP Reasoning in the Monotone μ-Calculus
Notes on Prolog Program Transformations, Prolog Style, and Efficient Compilation to The Warren Abstract Machine
Automatic Construction of Special Purpose Programs
Conservative Query Normalization on Parallel Circumscription
ITP at Argonne National Laboratory
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking
Redirecting Proofs by Contradiction
System Description: Similarity-Based Lemma Generation for Model Elimination
Logic-Independent Proof Search in Logical Frameworks - (Short Paper)
Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications
A Natural Proof System Based on rewriting Techniques
The Hybrid µ-Calculus
TeMP: A Temporal Monodic Prover
The TPTP Problem Library
A Tableau System for Quasi-Hybrid Logic
And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL
OSCAR
Extensions to a Generalization Critic for Inductive Proof
Classical Logic with Partial Functions
A Look at TPS
ACE: The Abstract Clause Engine
A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler
A Fresh Inductive Approach to Useful Call-by-Value
Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, July 19th, 2018
Verifying Refutations with Extended Resolution
Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
Jape: A Calculator for Animating Proof-on-Paper
Automated Induction with Constrained Tree Automata
A Resolution Calculus for Second-order Logic with Eager Unification
FaCT++ Description Logic Reasoner: System Description
FORT 2.0
SPASS-SATT - A CDCL(LA) Solver
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
Pi: an Interactive Derivation Editor for the Calculus of Partial Inductive Definitions
Correctness of Program Transformations as a Termination Problem
NoMoRe : A System for Non-monotonic Reasoning with Logic Programs under Answer Set Semantics
Integer Induction in Saturation
Automating Leibniz's Theory of Concepts
SMTtoTPTP - A Converter for Theorem Proving Formats
SCL Clause Learning from Simple Models
Towards Approximative Most Specific Concepts by Completion for EL with Subjective Probabilities
MædMax: A Maximal Ordered Completion Tool
Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic
The Inverse Method Implements the Automata Approach for Modal Satisfiability
Certificate Translation
Bit Inference
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
Symlog: Automated Advice in Fitch-style Proof Construction
Learn Omega-matic: System Description
Tutorial on Equational Unification
KBCV - Knuth-Bendix Completion Visualizer
Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics
Automatic Generation of Proof Search Strategies for Second-order Logic
Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
Quantomatic: A Proof Assistant for Diagrammatic Reasoning
Using Automated Theorem Provers to Certify Auto-generated Aerospace Software
System Description: TPS: A Theorem Proving System for Type Theory
Deciding Monodic Fragments by Temporal Resolution
Terminating Minimal Model Generation Procedures for Propositional Modal Logics
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
MCMT in the Land of Parametrized Timed Automata
Algebra and Automated Deduction
Hierarchical Reasoning for the Verification of Parametric Systems
Evidential Group Decision Making Model with Belief-Based Preferences
A Parallel Completion Procedure for Term Rewriting Systems
Combination of Unification Algorithms
On the Normalization and Unique Normalization Properties of Term Rewrite Systems
Purely Functional Implementation of a Logic
Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings
Advances in Proving Program Termination and Liveness
A Linear Time Algorithm for a Subcase of Second Order Instantiation
sKizzo: A Suite to Evaluate and Certify QBFs
Path Indexing for AC-Theories
Efficient Translation of Sequent Calculus Proofs Into Natural Deduction Proofs
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
An Improvement of Deduction Plans: Refutation Plans
Cycle Unification
Connection-Based Proof Search in Propositional BI Logic
An Introduction to Geometry Expert
CTL Model Checking in Deduction Modulo
Towards Fully Automated Axiom Extraction for Finite-Valued Logics
Specifying and Reasoning About Dynamic Access-Control Policies
A Practical Implementation of Simple Consequence Relations Using Inductive Definitions
Matching in a Class of Combined Non-disjoint Theories
On the Practical Value of Different Definitional Translations to Normal Form
Cooperating Proof Attempts
Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse
The CADE ATP System Competition
A Note on Resolution: How to Get Rid of Factoring without Loosing Completeness
Abstract Interpretation over Zones without Widening
System Description: Twelf - A Meta-Logical Framework for Deductive Systems
SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
IsaPlanner: A Prototype Proof Planner in Isabelle
KeY-C: A Tool for Verification of C Programs
A Formalisation of Finite Automata Using Hereditarily Finite Sets
On the Evaluation of Indexing Techniques for Theorem Proving
Many-valued Horn Logic is Hard
Combinable Extensions of Abelian Groups
The Potential of Interference-Based Proof Systems
Multi-Prover Verification of Floating-Point Programs
Extended Path-Indexing
Automated Cyclic Entailment Proofs in Separation Logic
A New Application for Explanation-Based Generalisation within Automated Deduction
PROTEIN: A PROver with a Theory Extension INterface
Evaluation of Axiom Selection Techniques
Handling Polymorphism in Automated Deduction
Exploitation of Parallelism in Prototypical Deduction Problems
Negative Paramodulation
Learning Conjecturing from Scratch
LOGICALC: An Environment for Interactive Proof Development
Mechanized Reasoning for Continuous Problem Domains (Invited Talk)
Implementing Verification Strategies in the KIV-System
Compatibility Formalization Between PR-OWL and OWL
Formalization of Continuous Probability Distributions
Datatypes with Shared Selectors
CASC-J3 - The 3rd IJCAR ATP System Competition
Omega: Towards a Mathematical Assistant
SYMEVAL: A Theorem Prover Based on the Experimental Logic
Combining Hilbert Style and Semantic Reasoning in a Resolution Framework
Extended Resolution Simulates DRAT
IMPS: System Description
On Deciding Satisfiability by DPLL(G+ T ) and Unsound Theorem Proving
Simulation Based Minimization
Decision Procedure for Autoepistemic Logic
DISSOLVER: A Dissolution-based Theorem Prover
Global Subsumption Revisited (Briefly)
System Description: An Interface Between CL A M and HOL
7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings
Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs
Sequent Calculi for Indexed Epistemic Logics
Automating Security Analysis: Symbolic Equivalence of Constraint Systems
Logical Matrix Generation and Testing
Adaptive Assertion-Level Proofs
Superposition for Lambda-Free Higher-Order Logic
KEIM: A Toolkit for Automated Deduction
A Unifying Splitting Framework
Deciding Intuitionistic Propositional Logic via Translation into Classical Logic
Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings
Automated Reasoning About Key Sets
Efficient Automated Reasoning About Sets and Multisets with Cardinality Constraints
EPR-Based Bounded Model Checking at Word Level
Modularity of Confluence
Real Analysis for Complex Systems
Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification
Individual Reuse in Description Logic Reasoning
Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms
ECR: An Equality Conditional Resolution Proof Procedure
A Uniform Substitution Calculus for Differential Dynamic Logic
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT
Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification
Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach
An AC-Compatible Knuth-Bendix Order
SPASS Version 3.5
Solving Bitvectors with MCSAT: Explanations from Bits and Pieces
Proceedings of 4th International Verification Workshop in connection with CADE-21, Bremen, Germany, July 15-16, 2007
Evonne: Interactive Proof Visualization for Description Logics (System Description)
Sine Qua Non for Large Theory Reasoning
Search Strategies for Resolution in Temporal Logics
An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012, Manchester, UK, June 30 - July 1, 2012
A Report of ARCADE 2017
Connections and Higher-Order Logic
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof
Difference Matching
iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
Evaluation of Systems for Higher-order Logic (ESHOL)
A General Method for Using Schematizations in Automated Deduction
SET Cardholder Registration: The Secrecy Proofs
NESCOND: An Implementation of Nested Sequent Calculi for Conditional Logics
A SAT-Based Approach to Learn Explainable Decision Sets
Relating Resolution and Algebraic Completion for Horn Logic
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
Theory-Specific Reasoning about Loops with Arrays using Vampire
Model Checking for Stability Analysis in Rely-Guarantee Proofs
Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2018), Oxford, UK, July 18, 2018
From the Universality of Mathematical Truth to the Interoperability of Proof Systems
System Description: Kimba, A Model Generator for Many-Valued First-Order Logics
Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures
THF0 - The Core of the TPTP Language for Higher-Order Logic
Reasoning About Vectors Using an SMT Theory of Sequences
Formal Reasoning About Influence in Natural Sciences Experiments
Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings
Extensional Higher-Order Paramodulation and RUE-Resolution
Unification and Matching Modulo Leaf-Permutative Equational Presentations
Challenges for Fast Synthesis Procedures in SMT
Terminating Tableaux for Hybrid Logic with Eventualities
A Logical Framework with Commutative and Non-commutative Subexponentials
A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code
Razor: Provenance and Exploration in Model-Finding
The Higher-Order Prover Leo-III
The Homer System
Automated Theorem Proving in a Simple Meta-Logic for LF
A System for Proving Equivalences of Recursive Programs
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
Reasoning About Exceptions in Ontologies: from the Lexicographic Closure to the Skeptical Closure
Cubicle- W : Parameterized Model Checking on Weak Memory
Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings
A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)
Disproving Conjectures
A New System and Methodology for Generating Random Modal Formulae
Left-Linear Completion with AC Axioms
Automated Reasoning, Fast and Slow
Exploring Predictability of SAT/SMT Solvers
Conditional Pure Literal Graphs
The Tree Width of Separation Logic with Recursive Definitions
A Sequent Calculus for Integer Arithmetic with Counterexample Generation
Towards Modularly Comparing Programs Using Automated Theorem Provers
ZPLAN: An Automatic Reasoning System for Situations
Verifying Safety Properties with the TLA+ Proof System
Distributed Theorem Proving by Peers
Reasoning in Non-normal Modal Description Logics
Collaborative Programming: Applications of Logic and Automated Reasoning
NP-Completeness of the Set Unification and Matching Problems
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings
Decidable Classes of Inductive Theorems
Constructive Hybrid Games
A Complete, Nonredundant Algorithm for Reversed Skolemization
10th International Workshop on Satisfiability Modulo Theories, SMT 2012, Manchester, UK, June 30 - July 1, 2012
An SMT-based approach to automated configuration
Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL
A New Method for Testing Decision Procedures in Modal Logics
Logic Machine Architecture: Inference Mechanisms
Security Protocols, Constraint Systems, and Group Theories
An Abstract View of Sorted Unification
An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions
Non-associative, Non-commutative Multi-modal Linear Logic
Sequoia: A Playground for Logicians - (System Description)
Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Prefixed Resolution: A Resolution Method for Modal and Description Logics
A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia
Improvements in Formula Generalization
Automated Higher-order Reasoning about Quantales
Primal Grammars and Unification Modulo a Binary Clause
Predictive Labeling with Dependency Pairs Using SAT
A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
Checkable Proofs for First-Order Theorem Proving
Truthful Monadic Abstractions
Extended Resolution as Certificates for Propositional Logic
On Symbol Elimination and Uniform Interpolation in Theory Extensions
Nominal Techniques in Isabelle/HOL
Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
Set of Support for Higher-Order Reasoning
System Description: Cooperation in Model Elimination: CPTHEO
Nuprl-Light: An Implementation Framework for Higher-Order Logics
An Assumption-Based Approach for Solving the Minimal S5-Satisfiability Problem
THINKER
The CHIP System: Constraint Handling In Prolog
The Abella Interactive Theorem Prover (System Description)
Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning
Automated Reasoning in the Simulation of Evolvable Systems
On Transfinite Knuth-Bendix Orders
Benchmarking Static Analyzers
Boolean Reasoning in a Higher-Order Superposition Prover
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
A Superposition View on Nelson-Oppen
Canonicity!
Parallel Theorem Proving with Connection Graphs
Program Termination Analysis by Size-Change Graphs (Abstract)
Certifying Safety and Termination Proofs for Integer Transition Systems
4th Workshop on Practical Aspects of Automated Reasoning, PAAR@IJCAR 2014, Vienna, Austria, 2014
Validating Mathematical Structures
Partitioning Methods for Satisfiability Testing on Large Formulas
The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting
Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems
Prover-independent Axiom Selection for Automated Theorem Proving in Ontohub
dL ι : Definite Descriptions in Differential Dynamic Logic
A Labelled System for IPL with Variable Splitting
Measuring Disagreement among Knowledge Bases
Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses
T-Decision by Decomposition
Termination Orderings for Rippling
Bitfields and Tagged Unions in C: Verification through Automatic Generation
Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
Strongly Analytic Tableaux for Normal Modal Logics
Confidences for Commonsense Reasoning
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs
The Decidability of the First-Order Theory of Knuth-Bendix Order
Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
Computer Search for Counterexamples to Wilkie's Identity
A Framework for Approximate Generalization in Quantitative Theories
Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Automatic Decidability and Combinability Revisited
Inferring Network Invariants Automatically
Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic
Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting
Proceedings of the Workshop on Type-Theoretic Languages: Proof Search and Semantics 2000, held in conjunction with CADE-17 Conference, Pittsburgh, PA, USA, June 20-21, 2000
Deciding Unique Termination of Permutative Rewriting Systems: Choose Your Term Algebra Carefully
adbmal
JGXYZ: An ATP System for Gap and Glut Logics
UNIF 2012 Post-Worskhop Proceedings. The 26th International Workshop on Unification, Manchester, UK, July 1, 2012
Efficient Model Construction for Horn Logic with VLog - System Description
A New Interpretation of the Resolution Principle
Partial Matching for Analogy Discovery in Proofs and Counter-Examples
Cocktail II
GEOTHER: A Geometry Theorem Prover
9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings
Global Caching for Coalgebraic Description Logics
How to Prove Equivalence of Term Rewriting Systems without Induction
Optimized Description Logic Reasoning via Core Blocking
Precise Dynamic Verification of Confidentiality
Hypergraph-Based Inference Rules for Computing EL + -Ontology Justifications
Temporal Logic for Proof-Carrying Code
Effective Finite-Valued Semantics for Labelled Calculi
Constraint Modelling: A Challenge for First Order Automated Reasoning (Invited Talk)
Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points
Progress in the Development of Automated Theorem Proving for Higher-Order Logic
Implementing Superposition in iProver (System Description)
First Order Reasoning on a Large Ontology
A New Approach to Universal Unification and Its Application to AC-Unification
Tabling for Higher-Order Logic Programming
A Formalization of a Concurrent Object Calculus up to alpha-Conversion
A Normative Supervisor for Reinforcement Learning Agents
PVS: A Prototype Verification System
Teaching Automated Theorem Proving by Example: PyRes 1.2 - (System Description)
CEL - A Polynomial-Time Reasoner for Life Science Ontologies
Probabilistic Logic Encoding of Spatial Domains
MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
RVF: An Automated Formal Verification System
Proving Pointer Programs in Higher-Order Logic
Partial Redundancy in Saturation
A Generalization of Semenov's Theorem to Automata over Real Numbers
On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewriting
Beyond DRAT: Challenges in Certifying UNSAT
Eliminating Dummy Elimination
Exact Kanowledge Compilation in Predicate Calculus: The Partial Achievement Case
MTT: The Maude Termination Tool (System Description)
Lexicographic Combination of Reduction Pairs
Sonic - Non-standard Inferences Go OilEd
Program Synthesis by Completion with Dependent Subtypes
Solving a Problem in Relevance Logic with an Automated Theorem Prover
Old or Heavy? Decaying Gracefully with Age/Weight Shapes
Termination and Reduction Checking for Higher-Order Logic Programs
What Can We Hope to Achieve From Automated Deduction? (Abstract)
A Saturation-based Algebraic Reasoner for ELQ
Linear Integer Arithmetic Revisited
Faster Proof Checking in the Edinburgh Logical Framework
What's Decidable About Arrays With Sums?
AC-Superposition with Constraints: No AC-Unifiers Needed
System Description: inka 5.0 - A Logic Voyager
Towards Strong Higher-Order Automation for Fast Interactive Verification
Program Verifier "Tatzelwurm": Reasoning about Systems of Linear Inequalities
Applications and Challenges in Satisfiability Modulo Theories
Translating between Language and Logic: What Is Easy and What Is Difficult
Weak Completion Semantics and its Applications in Human Reasoning
Unification and Matching Modulo Nilpotence
The Description Logic ALCNH R+ Extended with Concrete Domains: A Practically Motivated Approach
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis
A Fixedpoint Approach to Implementing (Co)Inductive Definitions
Advances and Challenges in the Development and Application of Forgetting Tools (invited talk abstract)
Proof Search and Certificates for Evidential Transactions
Monte Carlo Tableau Proof Search
A Resolution Theorem Prover for Intuitonistic Logic
JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants
LISS - The Logic Inference Search System
Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules