Interpolation systems for ground proofs in automated deduction: a survey (Q287275): Difference between revisions

@@ Property / Wikidata QID @@
+Q113901252
@@ Property / Wikidata QID: Q113901252 / rank @@
+Normal rank
@@ Property / cites work @@
+Lazy Abstraction with Interpolants for Arrays
@@ Property / cites work: Lazy Abstraction with Interpolants for Arrays / rank @@
+Normal rank
@@ Property / cites work @@
+New results on rewrite-based satisfiability procedures
+Normal rank
@@ Property / cites work @@
+A rewriting approach to satisfiability procedures.
+Normal rank
@@ Property / cites work @@
+Q4804899
@@ Property / cites work: Q4804899 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4737130
@@ Property / cites work: Q4737130 / rank @@
+Normal rank
@@ Property / cites work @@
+Abstract canonical inference
@@ Property / cites work: Abstract canonical inference / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite-Based Satisfiability Procedures for Recursive Data Structures
+Normal rank
@@ Property / cites work @@
+On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
+Normal rank
@@ Property / cites work @@
+On the modelling of search in theorem proving -- towards a theory of strategy analysis
+Normal rank
@@ Property / cites work @@
+On Interpolation in Decision Procedures
@@ Property / cites work: On Interpolation in Decision Procedures / rank @@
+Normal rank
@@ Property / cites work @@
+On interpolation in automated theorem proving
@@ Property / cites work: On interpolation in automated theorem proving / rank @@
+Normal rank
@@ Property / cites work @@
+Q5310200
@@ Property / cites work: Q5310200 / rank @@
+Normal rank
@@ Property / cites work @@
+An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
+Normal rank
@@ Property / cites work @@
+Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
+Normal rank
@@ Property / cites work @@
+A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints
+Normal rank
@@ Property / cites work @@
+From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
+Normal rank
@@ Property / cites work @@
+Quantifier-Free Interpolation of a Theory of Arrays
+Normal rank
@@ Property / cites work @@
+Quantifier-free interpolation in combinations of equality interpolating theories
+Normal rank
@@ Property / cites work @@
+Efficient generation of craig interpolants in satisfiability modulo theories
+Normal rank
@@ Property / cites work @@
+The relative efficiency of propositional proof systems
+Normal rank
@@ Property / cites work @@
+Linear reasoning. A new form of the Herbrand-Gentzen theorem
+Normal rank
@@ Property / cites work @@
+A machine program for theorem-proving
@@ Property / cites work: A machine program for theorem-proving / rank @@
+Normal rank
@@ Property / cites work @@
+A Computing Procedure for Quantification Theory
@@ Property / cites work: A Computing Procedure for Quantification Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient E-Matching for SMT Solvers
@@ Property / cites work: Efficient E-Matching for SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
+Normal rank
@@ Property / cites work @@
+Q2751361
@@ Property / cites work: Q2751361 / rank @@
+Normal rank
@@ Property / cites work @@
+Simplify: a theorem prover for program checking
@@ Property / cites work: Simplify: a theorem prover for program checking / rank @@
+Normal rank
@@ Property / cites work @@
+Propositional Interpolation and Abstract Interpretation
+Normal rank
@@ Property / cites work @@
+Interpolant Strength
@@ Property / cites work: Interpolant Strength / rank @@
+Normal rank
@@ Property / cites work @@
+Q4863622
@@ Property / cites work: Q4863622 / rank @@
+Normal rank
@@ Property / cites work @@
+Ground interpolation for the theory of equality
@@ Property / cites work: Ground interpolation for the theory of equality / rank @@
+Normal rank
@@ Property / cites work @@
+Q3743300
@@ Property / cites work: Q3743300 / rank @@
+Normal rank
@@ Property / cites work @@
+Modular proof systems for partial functions with Evans equality
+Normal rank
@@ Property / cites work @@
+Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
+Normal rank
@@ Property / cites work @@
+Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
+Normal rank
@@ Property / cites work @@
+Interpolation and Symbol Elimination in Vampire
@@ Property / cites work: Interpolation and Symbol Elimination in Vampire / rank @@
+Normal rank
@@ Property / cites work @@
+Ground Interpolation for Combined Theories
@@ Property / cites work: Ground Interpolation for Combined Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Abstractions from proofs
@@ Property / cites work: Abstractions from proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Playing in the grey area of proofs
@@ Property / cites work: Playing in the grey area of proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Q5528627
@@ Property / cites work: Q5528627 / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation and Symbol Elimination
@@ Property / cites work: Interpolation and Symbol Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
+Normal rank
@@ Property / cites work @@
+Some consequences of cryptographical conjectures for \(S_2^1\) and EF
+Normal rank
@@ Property / cites work @@
+An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
+Normal rank
@@ Property / cites work @@
+Automatic recognition of tractability in inference relations
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+An interpolating theorem prover
@@ Property / cites work: An interpolating theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Lazy Abstraction with Interpolants
@@ Property / cites work: Lazy Abstraction with Interpolants / rank @@
+Normal rank
@@ Property / cites work @@
+Quantified Invariant Generation Using an Interpolating Saturation Prover
+Normal rank
@@ Property / cites work @@
+Q4744264
@@ Property / cites work: Q4744264 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3677735
@@ Property / cites work: Q3677735 / rank @@
+Normal rank
@@ Property / cites work @@
+Simplification by Cooperating Decision Procedures
@@ Property / cites work: Simplification by Cooperating Decision Procedures / rank @@
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Lower bounds for resolution and cutting plane proofs and monotone computations
+Normal rank
@@ Property / cites work @@
+The Complexity of Propositional                                                   Proofs
@@ Property / cites work: The Complexity of Propositional Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Automated deduction for verification
@@ Property / cites work: Automated deduction for verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q5560258
@@ Property / cites work: Q5560258 / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation in local theory extensions
@@ Property / cites work: Interpolation in local theory extensions / rank @@
+Normal rank
@@ Property / cites work @@
+Proof theory
@@ Property / cites work: Proof theory / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank