On the generation of quantified lemmas (Q2417949): Difference between revisions

@@ Property / cites work @@
+Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars
+Normal rank
@@ Property / cites work @@
+Herbrand Confluence for First-Order Proofs with Π<sub>2</sub>-Cuts
+Normal rank
@@ Property / cites work @@
+On the Herbrand content of LK
@@ Property / cites work: On the Herbrand content of LK / rank @@
+Normal rank
@@ Property / cites work @@
+Herbrand's theorem as higher order recursion
@@ Property / cites work: Herbrand's theorem as higher order recursion / rank @@
+Normal rank
@@ Property / cites work @@
+Q4283227
@@ Property / cites work: Q4283227 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5331549
@@ Property / cites work: Q5331549 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751365
@@ Property / cites work: Q2751365 / rank @@
+Normal rank
@@ Property / cites work @@
+Rippling: Meta-Level Guidance for Mathematical Reasoning
+Normal rank
@@ Property / cites work @@
+The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
+Normal rank
@@ Property / cites work @@
+Q3006508
@@ Property / cites work: Q3006508 / rank @@
+Normal rank
@@ Property / cites work @@
+Algorithmic Compression of Finite Tree Languages by Rigid Acyclic Grammars
+Normal rank
@@ Property / cites work @@
+Inductive theorem proving based on tree grammars
@@ Property / cites work: Inductive theorem proving based on tree grammars / rank @@
+Normal rank
@@ Property / cites work @@
+System Description: GAPT 2.0
@@ Property / cites work: System Description: GAPT 2.0 / rank @@
+Normal rank
@@ Property / cites work @@
+Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs
+Normal rank
@@ Property / cites work @@
+Untersuchungen über das logische Schliessen. II
@@ Property / cites work: Untersuchungen über das logische Schliessen. II / rank @@
+Normal rank
@@ Property / cites work @@
+Introducing Quantified Cuts in Logic with Equality
+Normal rank
@@ Property / cites work @@
+Algorithmic introduction of quantified cuts
@@ Property / cites work: Algorithmic introduction of quantified cuts / rank @@
+Normal rank
@@ Property / cites work @@
+Towards Algorithmic Cut-Introduction
@@ Property / cites work: Towards Algorithmic Cut-Introduction / rank @@
+Normal rank
@@ Property / cites work @@
+Productive use of failure in inductive proof
@@ Property / cites work: Productive use of failure in inductive proof / rank @@
+Normal rank
@@ Property / cites work @@
+Conjecture synthesis for inductive theories
@@ Property / cites work: Conjecture synthesis for inductive theories / rank @@
+Normal rank
@@ Property / cites work @@
+The problem of \(\Pi_{2}\)-cut-introduction
@@ Property / cites work: The problem of \(\Pi_{2}\)-cut-introduction / rank @@
+Normal rank
@@ Property / cites work @@
+Incorporating Tables into Proofs
@@ Property / cites work: Incorporating Tables into Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Q3866101
@@ Property / cites work: Q3866101 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5624681
@@ Property / cites work: Q5624681 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5677085
@@ Property / cites work: Q5677085 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4215637
@@ Property / cites work: Q4215637 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5624680
@@ Property / cites work: Q5624680 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2711810
@@ Property / cites work: Q2711810 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3568690
@@ Property / cites work: Q3568690 / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic construction and verification of isotopy invariants
+Normal rank
@@ Property / cites work @@
+Lower Bounds on Herbrand's Theorem
@@ Property / cites work: Lower Bounds on Herbrand's Theorem / 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 @@
+Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 -- May 1, 2010. Revised selected papers
+Normal rank
@@ Property / cites work @@
+Atomic Cut Introduction by Resolution: Proof Structuring and Compression
+Normal rank