Download PDFOpen PDF in browser

Induction with Recursive Definitions in Superposition

EasyChair Preprint no. 6513

10 pagesDate: September 1, 2021


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.

Keyphrases: automated reasoning, first-order theorem proving, induction, saturation based proof search, structural induction, superposition reasoning, term algebra, Vampire

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Marton Hajdu and Petra Hozzová and Laura Kovacs and Andrei Voronkov},
  title = {Induction with Recursive Definitions in Superposition},
  howpublished = {EasyChair Preprint no. 6513},

  year = {EasyChair, 2021}}
Download PDFOpen PDF in browser