Proof generalization in \(\mathrm {LK}\) by second order unifier minimization (Q331619): Difference between revisions

@@ Property / cites work @@
+Resolution in type theory
@@ Property / cites work: Resolution in type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).
+Normal rank
@@ Property / cites work @@
+A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
+Normal rank
@@ Property / cites work @@
+The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
+Normal rank
@@ Property / cites work @@
+Q2751368
@@ Property / cites work: Q2751368 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem proving modulo
@@ Property / cites work: Theorem proving modulo / rank @@
+Normal rank
@@ Property / cites work @@
+A unification-theoretic method for investigating the \(k\)-provability problem
+Normal rank
@@ Property / cites work @@
+Q4539640
@@ Property / cites work: Q4539640 / rank @@
+Normal rank
@@ Property / cites work @@
+A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure
+Normal rank
@@ Property / cites work @@
+A Sequent Calculus with Implicit Term Representation
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+The number of proof lines and the size of proofs in first order logic
+Normal rank
@@ Property / cites work @@
+Positive and negative results for higher-order disunification
+Normal rank
@@ Property / cites work @@
+Analogy in inductive theorem proving
@@ Property / cites work: Analogy in inductive theorem proving / rank @@
+Normal rank
@@ Property / cites work @@
+A compact representation of proofs
@@ Property / cites work: A compact representation of proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Unification under a mixed prefix
@@ Property / cites work: Unification under a mixed prefix / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Science Logic
@@ Property / cites work: Computer Science Logic / rank @@
+Normal rank
@@ Property / cites work @@
+The epsilon calculus and Herbrand complexity
@@ Property / cites work: The epsilon calculus and Herbrand complexity / rank @@
+Normal rank
@@ Property / cites work @@
+Some Results on the Length of Proofs
@@ Property / cites work: Some Results on the Length of Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Pruning the search space and extracting more models in tableaux
+Normal rank
@@ Property / cites work @@
+A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
+Normal rank
@@ Property / cites work @@
+Proof theory. 2nd ed
@@ Property / cites work: Proof theory. 2nd ed / rank @@
+Normal rank
@@ Property / cites work @@
+Proving theorems by reuse
@@ Property / cites work: Proving theorems by reuse / rank @@
+Normal rank