Interpolation and Symbol Elimination (Q5191103): Difference between revisions

@@ 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/978-3-642-02959-2_17
+Normal rank
@@ Property / OpenAlex ID @@
+W1515795741
@@ Property / OpenAlex ID: W1515795741 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751353
@@ Property / cites work: Q2751353 / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient Interpolant Generation in Satisfiability Modulo Theories
+Normal rank
@@ Property / cites work @@
+Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
+Normal rank
@@ Property / cites work @@
+Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
+Normal rank
@@ Property / cites work @@
+Decision procedures for extensions of the theory of arrays
+Normal rank
@@ Property / cites work @@
+Cover Algorithms and Their Combination
@@ Property / cites work: Cover Algorithms and Their Combination / rank @@
+Normal rank
@@ Property / cites work @@
+Abstractions from proofs
@@ Property / cites work: Abstractions from proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Q5581665
@@ Property / cites work: Q5581665 / rank @@
+Normal rank
@@ Property / cites work @@
+Integrating Linear Arithmetic into Superposition Calculus
+Normal rank
@@ Property / cites work @@
+An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
+Normal rank
@@ Property / cites work @@
+An interpolation theorem in the predicate calculus
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Quantified Invariant Generation Using an Interpolating Saturation Prover
+Normal rank
@@ Property / cites work @@
+Equality and lyndon's interpolation theorem
@@ Property / cites work: Equality and lyndon's interpolation theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751359
@@ Property / cites work: Q2751359 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150300
@@ Property / cites work: Q3150300 / rank @@
+Normal rank
@@ Property / cites work @@
+Constraint Solving for Interpolation
@@ Property / cites work: Constraint Solving for Interpolation / 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 @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank