On the generation of quantified lemmas

DOI10.1007/s10817-018-9462-8zbMath1459.03011OpenAlexW2790318756WikidataQ124801826 ScholiaQ124801826MaRDI QIDQ2417949

Gabriel Ebner, Stefan Hetzl, Giselle Reis, Daniel Weller, Alexander Leitsch

Publication date: 31 May 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-018-9462-8

zbMATH Keywords

proof theoryresolution calculusHerbrand's theoremcut-introductionlemma generation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Unnamed Item ⋮ Higher-order pattern generalization modulo equational theories ⋮ On the cover complexity of finite languages

Uses Software

• TPTP
• HR
• GAPT
• IsaCoSy

Cites Work

• Algorithmic introduction of quantified cuts
• Conjecture synthesis for inductive theories
• Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 -- May 1, 2010. Revised selected papers
• The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
• Automatic construction and verification of isotopy invariants
• The problem of \(\Pi_{2}\)-cut-introduction
• Untersuchungen über das logische Schliessen. II
• Productive use of failure in inductive proof
• Herbrand's theorem as higher order recursion
• Inductive theorem proving based on tree grammars
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• System Description: GAPT 2.0
• Towards Algorithmic Cut-Introduction
• Atomic Cut Introduction by Resolution: Proof Structuring and Compression
• Introducing Quantified Cuts in Logic with Equality
• Incorporating Tables into Proofs
• Lower Bounds on Herbrand's Theorem
• Algorithmic Compression of Finite Tree Languages by Rigid Acyclic Grammars
• On the Herbrand content of LK
• Herbrand Confluence for First-Order Proofs with Π₂-Cuts
• Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars
• Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the generation of quantified lemmas