Hajdu, M., Hozzová, P., Kovács, L., & Voronkov, A. (2021). Induction with Recursive Definitions in Superposition. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (Vol. 2, pp. 246–255). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_34
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.
CC BY 4.0
