On the generation of quantified lemmas

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

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

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 theory; resolution calculus; Herbrand's theorem; cut-introduction; lemma generation

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

03F05: Cut-elimination and normal-form theorems

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Uses Software

• TPTP
• HR
• GAPT
• IsaCoSy