Induction with Recursive Definitions in Superposition

EasyChair Preprint 6513

Abstract

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: Vampire, automated reasoning, first-order theorem proving, induction, saturation based proof search, structural induction, superposition reasoning, term algebra

@booklet{EasyChair:6513,
  author    = {Marton Hajdu and Petra Hozzová and Laura Kovacs and Andrei Voronkov},
  title     = {Induction with Recursive Definitions in Superposition},
  howpublished = {EasyChair Preprint 6513},
  year      = {EasyChair, 2021}}