DC Field
Value
Language
dc.contributor.author
Hajdú, Márton
-
dc.contributor.author
Hozzová, Petra
-
dc.contributor.author
Kovács, Laura
-
dc.contributor.author
Schoisswohl, Johannes
-
dc.contributor.author
Voronkov, Andrei
-
dc.date.accessioned
2021-03-08T08:10:53Z
-
dc.date.available
2021-03-08T08:10:53Z
-
dc.date.issued
2020-07-26
-
dc.identifier.citation
<div class="csl-bib-body"> <div class="csl-entry">Hajdú, M., Hozzová, P., Kovács, L., Schoisswohl, J., &#38; 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.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.mimetype
application/pdf
-
item.fulltext
with Fulltext
-
item.openairetype
conference paper
-
item.openaccessfulltext
Open Access
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.grantfulltext
open
-
crisitem.project.funder
European Commission
-
crisitem.project.funder
European Commission
-
crisitem.project.funder
Fonds zur Förderung der wissenschaftlichen Forschung (FWF)
-
crisitem.project.funder
Vereine, Stiftungen, Preise
-
crisitem.project.grantno
639270
-
crisitem.project.grantno
842066
-
crisitem.project.grantno
W1255-N23
-
crisitem.author.dept
TU Wien
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192 - Institut für Logic and Computation
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.orcid
0000-0003-0845-5811
-
crisitem.author.orcid
0000-0002-8299-2714
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E180 - Fakultät für Informatik
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
Appears in Collections:
Conference Paper
Thumbnail
Hajdu - 2020 - Induction with generalization in superposition reasoning.pdf
Adobe PDF
(300.29 kB)
Postprint was published at CICM 2020.
Open Access
Show simple item record

Page view(s)

617
checked on Nov 23, 2023

Download(s)

163
checked on Nov 23, 2023

Google ScholarTM

Check