Stephan Falke and Deepak Kapur:
Inductive Decidability Using Implicit Induction
In Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '03), Phnom Penh, Cambodia.
Lecture Notes in Artificial Intelligence 4246, pages 45-59, 2006. ©Springer-Verlag
Decision procedures are widely used in automated reasoning tools in order to
reason about data structures. In applications, many
conjectures fall outside the theory handled by
a decision procedure.
Often, reasoning about user-defined functions on those data
structures is needed. For this, inductive reasoning has to be employed.
In this work, classes of function definitions and conjectures are
identified for which inductive validity can be automatically
decided using implicit induction methods and decision procedures for an
underlying theory.
The class of equational conjectures considered in this paper significantly
extends the results of Kapur & Subramaniam (CADE, 2000),
which were obtained using explicit induction schemes. Firstly, nonlinear
conjectures can be decided automatically.
Secondly, function definitions can use other defined functions in their
definitions, thus allowing mutually recursive functions and decidable
conjectures about them. Thirdly, conjectures
can have general terms from the decidable theory on inductive positions. These
contributions are crucial for successfully integrating inductive reasoning
into decision procedures, thus enabling their use in push-button mode
in applications including verification and program analysis.
[
BibTeX
|
Paper (ps.gz)
|
Paper (pdf)
|
Paper on SpringerLink
]