<div class="csl-bib-body">
<div class="csl-entry">Rawson, M., Wernhard, C., Zombori, Z., & Bibel, W. (2023). Lemmas: Generation, Selection, Application. In D. R. S. Ramanayake & J. Urban (Eds.), <i>Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings</i> (pp. 153–174). Springer. https://doi.org/10.1007/978-3-031-43513-3_9</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/190028
-
dc.description.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
dc.description.sponsorship
European Commission
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.subject
lemmas
en
dc.subject
automated reasoning
en
dc.subject
machine learning
en
dc.subject
condensed detachment
en
dc.subject
connection method
en
dc.title
Lemmas: Generation, Selection, Application
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.contributor.affiliation
Alfréd Rényi Institute of Mathematics, Hungary
-
dc.contributor.editoraffiliation
Czech Technical University in Prague, Czechia
-
dc.relation.isbn
978-3-031-43513-3
-
dc.relation.doi
10.1007/978-3-031-43513-3
-
dc.relation.issn
0302-9743
-
dc.description.startpage
153
-
dc.description.endpage
174
-
dc.relation.grantno
ERC Consolidator Grant 2020
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
tuw.booktitle
Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings
-
tuw.container.volume
14278
-
tuw.peerreviewed
true
-
tuw.book.ispartofseries
Lecture Notes in Computer Science
-
tuw.relation.publisher
Springer
-
tuw.relation.publisherplace
Cham
-
tuw.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publisher.doi
10.1007/978-3-031-43513-3_9
-
dc.description.numberOfPages
22
-
tuw.author.orcid
0000-0001-7834-1567
-
tuw.author.orcid
0000-0002-0438-8829
-
tuw.author.orcid
0000-0001-8622-5304
-
tuw.author.orcid
0000-0003-3892-0171
-
tuw.editor.orcid
0000-0002-7940-9065
-
tuw.event.name
TABLEAUX 2023: 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
en
dc.description.sponsorshipexternal
Deutsche Forschungsgemeinschaft
-
dc.description.sponsorshipexternal
North-German Supercomputing Alliance
-
dc.description.sponsorshipexternal
Hungarian National Excellence Grant
-
dc.description.sponsorshipexternal
Hungarian Artificial Intelligence National Laboratory Program
-
dc.relation.grantnoexternal
457292495
-
dc.relation.grantnoexternal
2018-1.2.1-NKP-00008
-
dc.relation.grantnoexternal
RRF-2.3.1-21-2022-00004
-
tuw.event.startdate
18-09-2023
-
tuw.event.enddate
21-09-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Prag
-
tuw.event.country
CZ
-
tuw.event.institution
Czech Technical University in Prague
-
tuw.event.presenter
Wernhard, Christoph
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
item.grantfulltext
none
-
item.fulltext
no Fulltext
-
item.cerifentitytype
Publications
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
