<div class="csl-bib-body">
<div class="csl-entry">Hajdu, M., Hozzova, P., Kovacs, L., & Voronkov, A. (2021). Induction with Recursive Definitions in Superposition. In <i>Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021</i> (Vol. 2, pp. 246–255). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_34</div>
</div>
Functional programs over inductively defined data
types, such as lists, binary trees and naturals, can naturally
be defined using recursive equations over recursive functions.
In first-order logic, function definitions can be considered as
universally quantified equalities. Verifying functional program
properties therefore requires inductive reasoning with both theories
and quantifiers. In this paper we propose new extensions
and generalizations to automate induction with recursive functions
in saturation-based first-order theorem proving, using the
superposition calculus. Instead of using function definitions as
first-order axioms, we introduced new simplification rules for
treating function definitions as rewrite rules. We guide inductive
reasoning and strengthen induction schema using recursively
defined functions. Our experimental results show that handling
recursive definitions in superposition reasoning significantly improves
automated reasoning with induction.
en
dc.language.iso
en
-
dc.relation.ispartofseries
Conference Series: Formal Methods in Computer-Aided Design
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
formal methods
en
dc.subject
computer-aided system design
en
dc.subject
hardware and system verification
en
dc.subject
formale Methode
de
dc.subject
rechnerunterstützte Systementwicklung
de
dc.subject
Hardwareverifikation
de
dc.title
Induction with Recursive Definitions in Superposition
en
dc.type
Beitrag in Tagungsband
de
dc.type
Inproceedings
en
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.identifier.doi
10.34727/2021/isbn.978-3-85448-046-4_34
-
dc.contributor.affiliation
University of Manchester, UK
-
dc.relation.isbn
978-3-85448-046-4
-
dc.relation.doi
10.34727/2021/isbn.978-3-85448-046-4
-
dc.description.volume
2
-
dc.description.startpage
246
-
dc.description.endpage
255
-
dc.type.category
Full-Paper Contribution
en
dc.type.category
Full-Paper-Beitrag
de
dc.relation.eissn
2708-7824
-
tuw.booktitle
Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021
-
tuw.peerreviewed
true
-
tuw.relation.haspart
10.34727/2021/isbn.978-3-85448-046-4
-
tuw.relation.publisher
TU Wien Academic Press
-
tuw.relation.publisherplace
Wien
-
tuw.book.chapter
34
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publication.orgunit
E194-05 - Forschungsbereich Compilers and Languages
-
dc.description.numberOfPages
10
-
tuw.relation.ispartoftuwseries
Conference Series: Formal Methods in Computer-Aided Design
-
tuw.author.orcid
0000-0002-8273-2613
-
tuw.author.orcid
0000-0003-0845-5811
-
tuw.author.orcid
0000-0002-8299-2714
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
tuw.event.name
Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design - FMCAD 2021
-
tuw.event.startdate
19-10-2021
-
tuw.event.enddate
22-10-2021
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
New Haven, Connecticut, USA
-
tuw.event.country
NON-EU
-
tuw.event.presenter
Hajdu, Marton
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.facultyfocus
Logic and Computation (LC)
de
wb.facultyfocus
Logic and Computation (LC)
en
wb.facultyfocus.faculty
E180
-
item.languageiso639-1
en
-
item.fulltext
with Fulltext
-
item.openaccessfulltext
Open Access
-
item.mimetype
application/pdf
-
item.openairetype
conference paper
-
item.grantfulltext
open
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.cerifentitytype
Publications
-
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