<div class="csl-bib-body">
<div class="csl-entry">Hajdú, M., Hozzová, P., Kovács, L., Schoisswohl, J., & Voronkov, A. (2020). Induction with Generalization in Superposition Reasoning. In <i>Proceedings of the 13th International Conference on Intelligent Computer Mathematics (CICM)</i> (pp. 123–137). Springer. https://doi.org/10.34726/961</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/16998
-
dc.identifier.uri
https://doi.org/10.34726/961
-
dc.description.abstract
We describe an extension of automating induction in superposition-based reasoning by strengthening inductive properties and generalizing terms over which induction should be applied. We implemented our approach in the first-order theorem prover Vampire and evaluated our work against state-of-the-art reasoners automating induction. We demonstrate the strength of our technique by showing that many interesting mathematical properties of natural numbers and lists can be proved automatically using this extension.
en
dc.description.sponsorship
European Research Council (ERC)
-
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
Austrian Science Fund (FWF)
-
dc.description.sponsorship
Vereine, Stiftungen, Preise
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
automated reasoning
en
dc.subject
induction
en
dc.subject
first-order theorem proving
en
dc.title
Induction with Generalization in Superposition Reasoning
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Urheberrechtsschutz
de
dc.rights.license
In Copyright
en
dc.relation.publication
Proceedings of the 13th International Conference on Intelligent Computer Mathematics (CICM)
-
dc.identifier.doi
10.34726/961
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.contributor.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.relation.isbn
978-3-030-53517-9
-
dc.relation.doi
10.1007/978-3-030-53518-6
-
dc.description.startpage
123
-
dc.description.endpage
137
-
dc.relation.grantno
639270
-
dc.relation.grantno
842066
-
dc.relation.grantno
W1255-N23
-
dcterms.dateSubmitted
2020-05-25
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
Proceedings of the 13th International Conference on Intelligent Computer Mathematics (CICM)
-
tuw.container.volume
12236
-
tuw.peerreviewed
true
-
tuw.book.ispartofseries
Lecture Notes in Computer Science
-
tuw.relation.publisher
Springer
-
tuw.relation.publisherplace
Cham
-
tuw.version
am
-
tuw.project.title
Symbolic Computation and Automated Reasoning for Program Analysis
-
tuw.project.title
Symbol Elimination in Reliable System Engineering
-
tuw.project.title
Doktoratskolleg
-
tuw.project.title
Domänenspezifisches Schließen in IoT Anwendungen
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publisher.doi
10.1007/978-3-030-53518-6_8
-
dc.identifier.libraryid
AC17203908
-
dc.description.numberOfPages
15
-
tuw.author.orcid
0000-0003-0845-5811
-
tuw.author.orcid
0000-0002-8299-2714
-
tuw.author.orcid
0000-0003-1073-7615
-
dc.rights.identifier
Urheberrechtsschutz
de
dc.rights.identifier
In Copyright
en
tuw.relation.issn
0302-9743
-
tuw.relation.eissn
1611-3349
-
dc.description.sponsorshipexternal
Engineering and Physical Sciences Research Council (EPSRC)
-
dc.description.sponsorshipexternal
KAW Foundation
-
dc.relation.grantnoexternal
EP/P03408X/1
-
dc.relation.grantnoexternal
Wallenberg Academy fellowship 2014 TheProSE
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openaccessfulltext
Open Access
-
item.openairetype
conference paper
-
item.fulltext
with Fulltext
-
item.mimetype
application/pdf
-
item.languageiso639-1
en
-
item.grantfulltext
open
-
item.cerifentitytype
Publications
-
crisitem.author.dept
TU Wien
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
University of Manchester
-
crisitem.author.orcid
0000-0003-0845-5811
-
crisitem.author.orcid
0000-0002-8299-2714
-
crisitem.author.orcid
0000-0003-1073-7615
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.project.funder
European Commission
-
crisitem.project.funder
European Commission
-
crisitem.project.funder
Fonds zur Förderung der wissenschaftlichen Forschung (FWF)
