Record link: 
http://hdl.handle.net/20.500.12708/190028
-
Title: 
Lemmas: Generation, Selection, Application
en
Citation: 
Rawson, M., Wernhard, C., Zombori, Z., & Bibel, W. (2023). Lemmas: Generation, Selection, Application. In D. R. S. Ramanayake & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 153–174). Springer. https://doi.org/10.1007/978-3-031-43513-3_9
-
Publisher DOI: 
10.1007/978-3-031-43513-3_9
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Rawson, Michael 
Wernhard, Christoph 
Zombori, Zsolt 
Bibel, Wolfgang 
-
Organisational Unit: 
E192 - Institut für Logic and Computation 
E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
-
Published in: 
Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings 
-
ISBN: 
978-3-031-43513-3
-
Volume: 
14278
-
DOI of the book: 
10.1007/978-3-031-43513-3
-
Date (published): 
14-Sep-2023
-
Event name: 
TABLEAUX 2023: 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods 
en
Event date: 
18-Sep-2023 - 21-Sep-2023
-
Event place: 
Prag, Czechia
-
Number of Pages: 
22
-
Publisher: 
Springer, Cham
-
Peer reviewed: 
Yes
-
Keywords: 
lemmas; automated reasoning; machine learning; condensed detachment; connection method
en
Abstract: 
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.
en
Project title: 
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission) 
-
Project (external): 
Deutsche Forschungsgemeinschaft
North-German Supercomputing Alliance
Hungarian National Excellence Grant
Hungarian Artificial Intelligence National Laboratory Program
-
Project ID: 
457292495
2018-1.2.1-NKP-00008
RRF-2.3.1-21-2022-00004
-
Research Areas: 
Logic and Computation: 100%
-
Science Branch: 
1020 - Informatik: 80%
1010 - Mathematik: 20%
-
Appears in Collections:
Conference Paper

Show full item record

Page view(s)

139
checked on Dec 1, 2023

Google ScholarTM

Check