On interpolation in automated theorem proving (Q2352502): Difference between revisions

@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SIMPLIFY
@@ Property / describes a project that uses: SIMPLIFY / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-014-9314-0
+Normal rank
@@ Property / OpenAlex ID @@
+W2064300892
@@ Property / OpenAlex ID: W2064300892 / rank @@
+Normal rank
@@ Property / cites work @@
+Modal languages and bounded fragments of predicate logic
+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 @@
+Methods of cut-elimination
@@ Property / cites work: Methods of cut-elimination / rank @@
+Normal rank
@@ Property / cites work @@
+Heaps and Data Structures: A Challenge for Automated Provers
+Normal rank
@@ Property / cites work @@
+A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
+Normal rank
@@ Property / cites work @@
+Superposition as a decision procedure for timed automata
+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 @@
+Interpolation systems for ground proofs in automated deduction: a survey
+Normal rank
@@ Property / cites work @@
+On deciding satisfiability by theorem proving with speculative inferences
+Normal rank
@@ Property / cites work @@
+Q5310200
@@ Property / cites work: Q5310200 / rank @@
+Normal rank
@@ Property / cites work @@
+From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
+Normal rank
@@ Property / cites work @@
+Quantifier-free interpolation in combinations of equality interpolating theories
+Normal rank
@@ Property / cites work @@
+On the mechanical derivation of loop invariants
@@ Property / cites work: On the mechanical derivation of loop invariants / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient generation of craig interpolants in satisfiability modulo theories
+Normal rank
@@ Property / cites work @@
+Linear reasoning. A new form of the Herbrand-Gentzen theorem
+Normal rank
@@ Property / cites work @@
+Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
+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 @@
+Model-based Theory Combination
@@ Property / cites work: Model-based Theory Combination / 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 @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolant Strength
@@ Property / cites work: Interpolant Strength / rank @@
+Normal rank
@@ Property / cites work @@
+Combinations of Theories for Decidable Fragments of First-Order Logic
+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 @@
+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 @@
+Interpolation and Symbol Elimination in Vampire
@@ Property / cites work: Interpolation and Symbol Elimination in Vampire / 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 @@
+Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
+Normal rank
@@ Property / cites work @@
+Interpolation and Symbol Elimination
@@ Property / cites work: Interpolation and Symbol Elimination / rank @@
+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 @@
+Quantified Invariant Generation Using an Interpolating Saturation Prover
+Normal rank
@@ Property / cites work @@
+Simplification by Cooperating Decision Procedures
@@ Property / cites work: Simplification by Cooperating Decision Procedures / rank @@
+Normal rank
@@ Property / cites work @@
+System Description: E 1.8
@@ Property / cites work: System Description: E 1.8 / 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 @@
+Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
+Normal rank