Labelled Clauses
Tal Lev-Ami, Christoph Weidenbach, Thomas Reps, and Mooly Sagiv
We add labels to first-order clauses to simultaneously apply
superpositions to several proof obligations inside one clause
set. From a theoretical perspective, the approach unifies a variety of
deduction modes. These include different strategies such as set of
support, as well as explicit case analysis, e.g., splitting. From a
practical perspective, labelled clauses offer advantages in the case
of related proof obligations resulting from multiple conjectures over
the same axiom set or from a single conjecture that is a large
conjunction. Here we can share clauses (e.g., the axioms and clauses
deduced from them, share Skolem symbols), share deduced clause
variants, and transfer lemmas between the different
obligations. Motivated by software verification, we have created a
prototype implementation of labelled clauses that supports multiple
conjectures, and we provide convincing experiments for the benefits.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)
University of Wisconsin