Q5094130 (Q5094130): Difference between revisions

@@ Property / describes a project that uses @@
+Mcmt
@@ Property / describes a project that uses: Mcmt / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation systems for ground proofs in automated deduction: a survey
+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 @@
+Term Rewriting and All That
@@ Property / cites work: Term Rewriting and All That / rank @@
+Normal rank
@@ Property / cites work @@
+Model theory.
@@ Property / cites work: Model theory. / rank @@
+Normal rank
@@ Property / cites work @@
+Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
+Normal rank
@@ Property / cites work @@
+Interpolant Strength
@@ Property / cites work: Interpolant Strength / rank @@
+Normal rank
@@ Property / cites work @@
+Cover Algorithms and Their Combination
@@ Property / cites work: Cover Algorithms and Their Combination / rank @@
+Normal rank
@@ Property / cites work @@
+MCMT: A Model Checker Modulo Theories
@@ Property / cites work: MCMT: A Model Checker Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
+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 @@
+Shostak's congruence closure as completion
@@ Property / cites work: Shostak's congruence closure as completion / rank @@
+Normal rank
@@ Property / cites work @@
+Conditional congruence closure over uninterpreted and interpreted symbols
+Normal rank
@@ Property / cites work @@
+An interpolation theorem in the predicate calculus
+Normal rank
@@ Property / cites work @@
+Lazy Abstraction with Interpolants
@@ Property / cites work: Lazy Abstraction with Interpolants / 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 @@
+On an interpretation of second order quantification in first order intuitionistic propositional logic
+Normal rank
@@ Property / cites work @@
+Lower bounds for resolution and cutting plane proofs and monotone computations
+Normal rank
@@ Property / cites work @@
+Deciding Combinations of Theories
@@ Property / cites work: Deciding Combinations of Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolant Strength Revisited
@@ Property / cites work: Interpolant Strength Revisited / rank @@
+Normal rank