First-order automated reasoning with theories: when deduction modulo theory meets practice
From MaRDI portal
Publication:2209546
DOI10.1007/s10817-019-09533-zzbMath1468.68282OpenAlexW2975454041WikidataQ127218472 ScholiaQ127218472MaRDI QIDQ2209546
Olivier Hermant, Guillaume Burel, Guillaume Bury, David Delahaye, Pierre Halmagrand, Raphaël Cauderlier
Publication date: 2 November 2020
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-019-09533-z
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (3)
Automated reasoning with restricted intensional sets ⋮ A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
Uses Software
Cites Work
- The foundations of mathematics. A study in the philosophy of science
- Resolution is cut-free
- Lattice-valued representation of the cut-elimination theorem
- Refutational theorem proving for hierarchic first-order theories
- Theorem proving modulo
- Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
- Autarkic computations in formal proofs
- Cooperation of background reasoners in theory reasoning by residue sharing
- Automated deduction by theory resolution
- Regaining cut admissibility in deduction modulo using abstract completion
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Semantic tableaux with equality
- Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
- The TPTP Typed First-Order Form with Arithmetic
- Tableaux Modulo Theories Using Superdeduction
- Encoding Monomorphic and Polymorphic Types
- Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
- Polarized Resolution Modulo
- Satisfiability Modulo Theories
- Soundly Proving B Method Formulæ Using Typed Sequent Calculus
- ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti
- Completeness and Cut-elimination in the Intuitionistic Theory of Types
- Beagle – A Hierarchic Superposition Theorem Prover
- Integrating Simplex with Tableaux
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Simplify: a theorem prover for program checking
- Embedding Deduction Modulo into a Prover
- Coq Modulo Theory
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Efficient E-Matching for SMT Solvers
- Superdeduction at Work
- On Constructive Cut Admissibility in Deduction Modulo
- Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
- First-Order Logic with Dependent Types
- Deciding Combinations of Theories
- Fast Decision Procedures Based on Congruence Closure
- Simplification by Cooperating Decision Procedures
- Logic Programming with Focusing Proofs in Linear Logic
- A framework for defining logics
- The B-Book
- Incremental theory reasoning methods for semantic tableaux
- Proof normalization modulo
- Hierarchic Superposition with Weak Abstraction
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- Cut Admissibility by Saturation
- Automated Reasoning
- Automated Reasoning
- A Semantic Completeness Proof for TaMeD
- Theory Instantiation
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- A Machine-Oriented Logic Based on the Resolution Principle
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Term Rewriting and Applications
- Typed Lambda Calculi and Applications
- An Automation-Friendly Set Theory for the B Method
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: First-order automated reasoning with theories: when deduction modulo theory meets practice
