yusuke1997/dblp-id-title huggingface dataset:
Loopfrog - loop summarization for static analysis
Some Results on Equational Unification
Biabduction (and Related Problems) in Array Separation Logic
A Termination Checker for Isabelle Hoare Logic
Improving ENIGMA-style Clause Selection while Learning From History
The Use of Proof Plans to Sum Series
Built-in Variant Generation and Unification, and Their Applications in Maude 2.7
(Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems
8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings
Deciding ATL * Satisfiability by Tableaux
Conservative Extensions in the Lightweight Description Logic EL
Computing Tiny Clause Normal Forms
How to Prove Inductive Theorems? QUODLIBET!
The 2nd Verified Software Competition: Experience Report
Deciding Combinations of Theories
Broadening the Scope of SMT-COMP: the Application Track
Constructive Decision via Redundancy-Free Proof-Search
Non-clausal Redundancy Properties
Quati: An Automated Tool for Proving Permutation Lemmas
The Isabelle/Naproche Natural Language Proof Assistant
Proving the Chinese Remainder Theorem by the Cover Set Induction
Second-Order Logic over Finite Structures - Report on a Research Programme
Automating Inductive Proofs Using Theory Exploration
ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output
Dynamic Behavior Matching: A Complexity Analysis and New Approximation Algorithms
The ICS Decision Procedures for Embedded Deduction
System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog
Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013
Completeness and Decidability Results for First-Order Clauses with Indices
Canonical Forms and Unification
Monotonicity Inference for Higher-Order Formulas
Cylindric Algebra Equation Solver
Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning, Cork, Ireland, July 4-8, 2004
System Description: Generating Models by SEM
First-Order Theorem Proving Using Conditional Rewrite Rules
Towards Efficient Subsumption
A Separation Logic with Data: Small Models and Automation
Checking Natural Language Proofs
Automatic Generation of Logical Models with AGES
Effective Normalization Techniques for HOL
A New Logic for Jointly Representing Hard and Soft Constraints
Higher Order E-Unification
A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems
Argument-Bounded Algorithms as a Basis for Automated Termination Proofs
System Description: E-KRHyper
Ordered Chaining for Total Orderings
Deduction as a Service
Restricted Combinatory Unification
AI at CADE/IJCAR
Procedural Interpretation of Non-Horn Logic Programs
Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic
Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards
A Complete Semantic Back Chaining Proof System
Proceedings of the Second Workshop on Logics for Reasoning about Preferences, Uncertainty, and Vagueness co-located with the 9th International Joint Conference on Automated Reasoning, PRUV@IJCAR 2018, Oxford, UK, July 19th, 2018
Eves System Description
Temporalizing Ontology-Based Data Access
Verified Approximation Algorithms
Mechanical Verification of Mutually Recursive Procedures
Preservation of Proof Obligations from Java to the Java Virtual Machine
Generation of Parametrically Uniform Knowledge Bases in a Relational Probabilistic Logic with Maximum Entropy Semantics
A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
Decidability Results for Saturation-Based Model Building
QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability
Embedding Lax Logic into Intuitionistic Logic
Focussing, MALL and the Polynomial Hierarchy
Analyzing Selected Quantified Integer Programs
Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival
Perfect Discrimination Graphs: Indexing Terms with Integer Exponents
Proof Support for Common Logic
Grammar Specification in Categorial Logics and Theorem Proving
Case-Free Programs: An Abstraction of Definite Horn Programs
Unifying Decidable Entailments in Separation Logic with Inductive Definitions
System Description: E-KRHyper 1.4 - Extensions for Unique Names and Description Logic
SiCoTHEO: Simple Competitive Parallel Theorem Provers
Computing k-Rank Answers with Ontological CP-Nets
My Life with an Automatic Theorem Prover
Scala to the Power of Z3: Integrating SMT and Programming
System Description: Using OBDD's for the validation of Skolem verification conditions
Dr.Doodle: A Diagrammatic Theorem Prover
Using Matings for Pruning Connection Tableaux
Unification Modulo Synchronous Distributivity
Formulation of Induction Formulas in Verification of Prolog Programs
Transforming Matings into Natural Deduction Proofs
A High-Performance Parallel Theorem Prover
Isabelle: The Next Seven Hundred Theorem Provers
Improving Assoviative Path Orderings
Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables
Resolution and Quantified Epistemic Logics
Inductive Beluga: Programming Proofs
A FOOLish Encoding of the Next State Relations of Imperative Programs
Regular Patterns in Second-Order Unification
Rewriting Induction + Linear Arithmetic = Decision Procedure
Stratified Resolution
Model Stack for the Pervasive Verification of a Microkernel-based Operating System
Little Theories
Prolog Technology Reinforcement Learning Prover - (System Description)
Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules
Machine Instruction Syntax and Semantics in Higher Order Logic
Some Thoughts About FOL-Translations in Vampire
Solving for Set Variables in Higher-Order Theorem Proving
Algebraically Closed Fields in Isabelle/HOL
Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems
SATO: An Efficient Propositional Prover
A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories
PARTHEO: A High-Performance Parallel Theorem Prover
StarExec: A Cross-Community Infrastructure for Logic Solving
Unification in Many-Sorted Eqational Theories
Translating Between Implicit and Explicit Versions of Proof
Linear-Input Subset Analysis
The 481 Ways to Split a Clause and Deal with Propositional Variables
On Automating the Calculus of Relations
Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings
Lotrec : The Generic Tableau Prover for Modal and Description Logics
Patching Faulty Conjectures
Resolution-Based Calculi for Modal and Temporal Logics
First-Order Logic with Dependent Types
Redundancy Notions for Paramodulation with Non-monotonic Orderings
Extensional Higher-Order Resolution
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings
Formalizing Undefinedness Arising in Calculus
Translating Scala Programs to Isabelle/HOL - System Description
The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints
Paraconsistent Gödel Modal Logic
NEXPTIME-Complete Description Logics with Concrete Domains
Tutorial: Automated Deduction and Natural Language Understanding
Dependency Pairs for Rewriting with Non-free Constructors
DDDLIB: A Library for Solving Quantified Difference Inequalities
Automated Analysis of Regular Algebra
Solving Equational Problems Efficiently
Presenting Proofs in a Human-Oriented Way
An Incremental Technique for Automata-Based Decision Procedures
nanoCoP: A Non-clausal Connection Prover
A Polymorphic Vampire - (Short Paper)
TPTP and Beyond: Representation of Quantified Non-Classical Logics
Compilation as Rewriting in Higher Order Logic
A Classification of Many-Sorted Unification Problems
Computing Prime Implicants
Advanced Indexing Operations on Substitution Trees
Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures
Substitution-based Compilation of Extended Rules in Deductive Databases
Sufficient Completness, Term Rewriting Systems and "Anti-Unification"
A Decision Method for Linear Temporal Logic
Optimized Query Rewriting for OWL 2 QL
Induction using Term Orderings
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Invited talk: Developing Efficient SMT Solvers
High-Level Verification Using Theorem Proving and Formalized Mathematics
Maslov's Class K Revisited
SETHEO Goes Software Engineering: Application of ATP to Software Reuse
Combination of Distributed Search and Multi-search in Peers-mcd.d
Proving Properties of Incremental Merkle Trees
Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving
Proving Non-looping Non-termination Automatically
Tutorial on Lambda-Prolog
Labelled Clauses
TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism
Reuse in Software Verification by Abstract Method Calls
A Focused Sequent Calculus for Higher-Order Logic
Resolution and Clause Learning for Multi-Valued CNF Formulas
Comparison of Natural Deduction and Locking Resolution Implementations
An Experimental Pipeline for Automated Reasoning in Natural Language (Short Paper)
Different Proofs are Good Proofs
SAT solving experiments in Vampire
A Classification of Non-liftable Orders for Resolution
Proceedings of the First International Workshop on Uncertainty in Description Logics, Edinburgh, UK, July 20, 2010
Reconstruction Proofs at the Assertion Level
SCOTT: Semantically Constrained Otter System Description
CDCL with Less Destructive Backtracking through Partial Ordering
Program Synthesis Using Dual Interpretation
Scavenger 0.1: A Theorem Prover Based on Conflict Resolution
Contextual Rewriting in SPASS
Proving System Correctness with KIV 3.0
Real World Verification
ATx'12/WInG'12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation, Manchester, UK, June 2012
TRSPEC: A Term Rewriting Based System for Algebraic Specifications
Instantiation-Based Automated Reasoning: From Theory to Practice
On Indefinite Databases and the Closed World Assumption
Theorem Proving in Dependently-Typed Higher-Order Logic
Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract)
Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability
Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
HyLoRes 1.0: Direct Resolution for Hybrid Logics
On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics E ℒ, E ℒ +
Converting Non-Classical Matrix Proofs into Sequent-Style Systems
A Framework for Cooperating Decision Procedures
Initial Experiments on Deriving a Complete HOL Simplification Set
veriT: An Open, Trustable and Efficient SMT-Solver
Backward Trace Slicing for Rewriting Logic Theories
Complexity of the higher order matching
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
On the Connection between Narrowing and Proof by Consistency
ROO: A Parallel Theorem Prover
Efficient Instance Retrieval with Standard and Relational Path Indexing
Data Structures and Control Architectures for Implementation of Theorem-Proving Programs
Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
Mind the Gap: Formal Verification and the Common Criteria (Discussion Paper)
Exploiting parallelism in the ME calculus
A Progress Report on New Decision Algorithms for Finitely Prsented Abelian Groups
On Unification for Bonded Distributive Lattices
Synthesis of Induction Orderings for Existence Proofs
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007
Better Proof Output for Vampire
DELTA - A Bottom-up Preprocessor for Top-Down Theorem Provers - System Abstract
Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol
Reasoning about Quantifiers by Matching in the E-graph
A Resolution-Based Calculus for Preferential Logics
Linear Quantifier Elimination as an Abstract Decision Procedure
Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4
On the Relationship Between Non-Horn Magic Sets and Relevancy Testing
A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method
Interpolation and Symbol Elimination in Vampire
Automatic Verification of Cryptographic Protocols with SETHEO
The Theorem Prover of the Program Verifier Tatzelwurm
Exponential Improvement of Efficient Backtracking: data Structure and Implementation
Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)
Logical Difference Computation with CEX2.5
Monadic Decomposition in Integer Linear Arithmetic
Unification in the Data Structure Sets
Approximations for Model Construction
Extending SMT Solvers to Higher-Order Logic
Using Vampire in Soundness Proofs of Type Systems
System Description: LEO - A Higher-Order Theorem Prover
Adventures in Associative-Commutative Unification (A Summary)
Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan
The Model Evolution Calculus
More On Implicit Syntax
Stratified Context Unification Is NP-Complete
A New Equational Unification Method: A Generalization of Martelli-Montanari's Algorithm
Lemma Matching for a PTTP-based Top-down Theorem Prover
Ordered Rewriting and Confluence
Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I
On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables
Fault-Tolerant Distributed Theorem Proving
A Linear Characterization of NP-Complete Problems
SEPIA: Search for Proofs Using Inferred Automata
Lazy Generation of Induction Hypotheses
Lambda-Prolog: An Extended Logic Programming Language
A Knuth-Bendix-Like Ordering for Orienting Combinator Equations
SAT-Based Decision Procedure for Analytic Pure Sequent Calculi
Proof Generation in the Touchstone Theorem Prover
Tutorial: Meta-logical Frameworks
Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies
On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic
Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving
Integration of the TPTPWorld into SigmaKEE
An LCF-Style Interface between HOL and First-Order Logic
Scalable Knowledge Representation and Reasoning Systems
Proceedings of the 2nd International Workshop Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016)., Coimbra, Portugal, July 1, 2016
A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
Aligator: A Mathematica Package for Invariant Generation (System Description)
Deduction with XOR Constraints in Security API Modelling
Specification Predicates with Explicit Dependency Information
The New WALDMEISTER Loop at Work
Exploring Theories with a Model-Finding Assistant
Specifying Theorem Provers in a Higher-Order Logic Programming Language
FRI: Failure-Resistant Induction in RRL
Decision Procedures for Recursive Data Structures with Integer Constraints
The Tableau Browser SNARKS
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
Retrieving Library Identifiers via Equational Matching of Types
Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses
Proof Systems for Effectively Propositional Logic
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
The Passau RAP System: Prototyping Algebraic Specifications Using Conditional Narrowing
Knowledge Engineering for Large Ontologies with Sigma KEE 3.0
A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies
Games, Automata and Matching
The Power of the Church-Rosser Property for String Rewriting Systems
On Hierarchical Reasoning in Combinations of Theories
Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation
Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators in Isomorphism Complete
Detecting Inconsistencies in Large First-Order Knowledge Bases
Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, Manchester, United Kingdom, June 30, 2012
Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk)
Clause Redundancy and Preprocessing in Maximum Satisfiability
Composable Packages for Higher Order Logic Theories
SMT and Functional Equation Solving over the Reals: Challenges from the IMO
SPASS & FLOTTER Version 0.42
Cut Elimination for Negative Free Logics with Definite Descriptions
Embedding Negation as Failure into a Model Generation Theorem Prover
Probably Half True: Probabilistic Satisfiability over Łukasiewicz Infinitely-Valued Logic
Decision Procedures Customized for Formal Verification
Verified Interactive Computation of Definite Integrals
Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany, August 2, 2015
Improvements of a Tautology-Testing Algorithm
Sledgehammer: Judgement Day
Subset Types and Partial Functions
Incremental Rewriting Modulo SMT
Querying the Guarded Fragment via Resolution (Extended Abstract)
EFS - An Interactive Environment for Formal Systems
Presenting Machine-Found Proofs
Unification in Boolean Rings
A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited
History and Prospects for First-Order Automated Deduction
Workshop: Automation of Proofs by Mathematical Induction
Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into
Investigations into Proof-Search in a System of First-Order Dependent Function Types
A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality
Workshop: The Role of Automated Deduction in Mathematics
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Evaluation Opportunities in Mechanized Theories
Proving Termination of C Programs with Lists
System Description: Proof Planning in Higher-Order Logic with Lambda-Clam
Goéland: A Concurrent Tableau-Based Theorem Prover (System Description)
X.R.S : Explicit Reduction Systems - A First-Order Calculus for Higher-Order Calculi
Reasoning about Iteration in Gödel's Class Theory
Elimination of Equality via Transformation with Ordering Constraints
argo-lib: A Generic Platform for Decision Procedures
Equational Theorem Proving Modulo
CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems
Efficient Neural Clause-Selection Reinforcement
Optimizing Higher-Order Pattern Unification
Verified Given Clause Procedures
Cutting to the Chase Solving Linear Integer Arithmetic
Exploring Model-Based Development for the Verification of Real-Time Java Code
Simplifying Interpreted Formulas
Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion
Automatic Termination Proofs in the Dependency Pair Framework
MGTP: A Parallel Theorem Prover Based on Lazy Model Generation
Automated Invariant Generation for the Verification of Real-Time Systems
Reasoning with large numbers of individuals moves on: extending the instance store
Super-Blocked Clauses
More is Less: Adding Polynomials for Faster Explanations in NLSAT
Foundational Certified Code in a Metalogical Framework
On Restrictions of Ordered Paramodulation with Simplification
OTTER 2.0
A Practical Integration of First-Order Reasoning and Decision Procedures
A Theory of Arrays with set and copy Operations
A Logical Framework for Developing and Mechanizing Set Theories
Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems
Symbolic Fault Injection
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
Automatic Construction and Verification of Isotopy Invariants
Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT
Answering Ontological Ranking Queries Based on Subjective Reports
A Subsumption Algorithm Based on Characteristic Matrices
Overview of a Theorem-Prover for A Computational Logic
Efficient Model Generation through Compilation
Automated Theorem Proving for Assertions in Separation Logic with All Connectives
System Description: Interactive Proof Critics in XBarnacle
Lower Runtime Bounds for Integer Programs
Linear Quantifier Elimination
Generalised Handling of Variables in Disconnection Tableaux
GKC: A Reasoning System for Large Knowledge Bases
System Description: Multi A Multi-strategy Proof Planner
SAT-Based Proof Search in Intermediate Propositional Logics
Termination of Theorem Proving by Reuse
Tableaux for Temporal Description Logic with Constant Domains
Practical Aspects of SAT Solving
Tactical Theorem Proving in Program Verification
Grammar Rewriting
From Axioms to Proof Rules, then add Quantifiers
Focussing Proof-Net Construction as a Middleware Paradigm
Taking Satisfiability to the Next Level with Z3 - (Abstract)
Formalizing a Seligman-Style Tableau System for Hybrid Logic - (Short Paper)
Model Checking Using Tabled Rewriting
Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics
Representing Proof Transformations for Program Optimizations
Superposition and Chaining for Totally Ordered Divisible Abelian Groups
Building an Efficient OWL 2 DL Reasoner
Enumerating Justifications Using Resolution
Model Checking: New Challenges and Opportunities for Automated Reasoning (Invited Talk)
RACER System Description
About VeriFun
Automated Reasoning in ALCQ \mathcal{ALCQ} via SMT
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators with Simple Geometry
Efficient Interpolation for the Theory of Arrays
A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus
A Geometry Theorem Prover for Macintoshes
An Interactive Enhancement to the Boyer-Moore Theorem Prover
Proving Group Protocols Secure Against Eavesdroppers
What Do We Know When We Know That a Theory Is Consistent?
Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics
LP: The Larch Prover
MCMT: A Model Checker Modulo Theories
Implementing Different Proof Calculi for First-order Modal Logics
Animated Logic: Correct Functional Conversion to Conjunctive Normal Form
Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving
The FAUST - Prover
Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints
randoCoP: Randomizing the Proof Search Order in the Connection Calculus
A Method for Building Models Automatically. Experiments with an Extension of OTTER
The KeY system 1.0 (Deduction Component)
A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting
An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description
Fully Verified Java Card API Reference Implementation
Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
Modular Reasoning in Isabelle
Deciding Inductive Validity of Equations
Theorem Proving with Ordering Constrained Clauses
Soft Typing for Ordered Resolution
Certified Core-Guided MaxSAT Solving
Formalizing O Notation in Isabelle/HOL
A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
Volume Computation for Boolean Combination of Linear Arithmetic Constraints