Lemmas: Generation, Selection, Application

Autor:	Rawson, Michael, Wernhard, Christoph, Zombori, Zsolt, Bibel, Wolfgang
Rok vydání:	2023
Předmět:	Computer Science - Logic in Computer Science Computer Science - Artificial Intelligence
Druh dokumentu:	Working Paper
DOI:	10.1007/978-3-031-43513-3_9
Popis:	Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search. Comment: Extended version of the TABLEAUX 2023 contribution
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2303.05854 Zobrazit plný text záznamu View this record from Arxiv