학술논문
Getting saturated with induction.
Document Type
Proceedings Paper
Author
Hajdu, Márton (A-TUWN-NDM) AMS Author Profile; Hozzová, Petra (A-TUWN-NDM) AMS Author Profile; Kovács, Laura (A-TUWN-NDM) AMS Author Profile; Reger, Giles (4-MANC-NDM) AMS Author Profile; Voronkov, Andrei (A-TUWN-NDM) AMS Author Profile
Source
Subject
Language
English
Abstract
Summary: ``Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating induction directly into the saturation-based proof search framework of first-order theorem proving. We describe our induction inference rules proving properties with inductively defined datatypes and integers. We also present additional reasoning heuristics for strengthening inductive reasoning, as well as for using induction hypotheses and recursive function definitions for guiding induction. We present exhaustive experimental results demonstrating the practical impact of our approach as implemented within Vampire.''