학술논문
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 isa new exciting direction in the automation of inductive reasoning. Inthis paper we survey our work on integrating induction directly intothe saturation-based proof search framework of first-order theoremproving. We describe our induction inference rules proving propertieswith inductively defined datatypes and integers. We also presentadditional reasoning heuristics for strengthening inductive reasoning,as well as for using induction hypotheses and recursive functiondefinitions for guiding induction. We present exhaustive experimentalresults demonstrating the practical impact of our approach asimplemented within Vampire.''