A Coinduction Rule for Entailment of Recursively Defined Properties
Joxan Jaffar, Andrew Santosa and Razvan Voicu
Abstract
Recursively defined properties are ubiquitous. We present a proof
meth\-od for establishing entailment $\G \models \HH$ of such
properties $\G$ and $\HH$ over a set of common variables. The main
contribution is a particular proof rule based intuitively upon the
concept of {\it coinduction}. This rule allows the inductive step
of assuming that an entailment holds during the proof the
entailment. In general, the proof method is based on an unfolding
(and no folding) algorithm that reduces recursive definitions to a
point where only constraint solving is necessary. The
constraint-based proof obligation is then discharged with available
solvers. The algorithm executes the proof by a search-based method
which automatically discovers the opportunity of applying induction
instead of the user having to specify some induction schema, and
which does not require any base case.