Interpolation systems for ground proofs in automated deduction: a survey
From MaRDI portal
Publication:287275
DOI10.1007/s10817-015-9325-5zbMath1356.68179OpenAlexW2028087487WikidataQ113901252 ScholiaQ113901252MaRDI QIDQ287275
Maria Paola Bonacina, Moa Johansson
Publication date: 26 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-015-9325-5
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (8)
Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Craig interpolation with clausal first-order tableaux ⋮ On First-Order Model-Based Reasoning ⋮ Interpolation in extensions of first-order logic ⋮ Unnamed Item ⋮ Multicomponent proof-theoretic method for proving interpolation properties ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ On interpolation in automated theorem proving
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Some consequences of cryptographical conjectures for \(S_2^1\) and EF
- A rewriting approach to satisfiability procedures.
- On interpolation in automated theorem proving
- Modular proof systems for partial functions with Evans equality
- An interpolating theorem prover
- Rewrite-Based Satisfiability Procedures for Recursive Data Structures
- Ground interpolation for the theory of equality
- Quantifier-Free Interpolation of a Theory of Arrays
- Lazy Abstraction with Interpolants for Arrays
- From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
- Playing in the grey area of proofs
- Efficient generation of craig interpolants in satisfiability modulo theories
- On Interpolation in Decision Procedures
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
- A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Abstractions from proofs
- Solving SAT and SAT Modulo Theories
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Simplify: a theorem prover for program checking
- Propositional Interpolation and Abstract Interpretation
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Efficient E-Matching for SMT Solvers
- Interpolation in local theory extensions
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Interpolant Strength
- Simplification by Cooperating Decision Procedures
- The relative efficiency of propositional proof systems
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- The Complexity of Propositional Proofs
- Ground Interpolation for Combined Theories
- Interpolation and Symbol Elimination
- Automated deduction for verification
- Abstract canonical inference
- New results on rewrite-based satisfiability procedures
- Automatic recognition of tractability in inference relations
- Automated Deduction – CADE-20
- Quantifier-free interpolation in combinations of equality interpolating theories
- On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Interpolation and Symbol Elimination in Vampire
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
- Lazy Abstraction with Interpolants
- Computer Aided Verification
- Proof theory
This page was built for publication: Interpolation systems for ground proofs in automated deduction: a survey
