Interpolation and Symbol Elimination in Vampire (Q5747760): 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 @@
+TPTP
@@ Property / describes a project that uses: TPTP / 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/978-3-642-14203-1_16
+Normal rank
@@ Property / OpenAlex ID @@
+W1744405537
@@ Property / OpenAlex ID: W1744405537 / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient Interpolant Generation in Satisfiability Modulo Theories
+Normal rank
@@ Property / cites work @@
+A framework for numeric analysis of array operations
+Normal rank
@@ Property / cites work @@
+Abstractions from proofs
@@ Property / cites work: Abstractions from proofs / rank @@
+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 @@
+Array Abstractions from Proofs
@@ Property / cites work: Array Abstractions from Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation and Symbol Elimination
@@ Property / cites work: Interpolation and Symbol Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Quantified Invariant Generation Using an Interpolating Saturation Prover
+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 @@
+The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
+Normal rank
@@ Property / cites work @@
+System Description: Spass Version 3.0
@@ Property / cites work: System Description: Spass Version 3.0 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5747760