Finite Semantic Trees Suffice for Ordered Resolution and
Paramodulation
Showing completeness of resolution and paramodulation strategies is
notoriously difficult. There are many techniques, among which Bachmair
and Ganzinger's model generation has been the most successfull during
the last decade. Our goal in this paper is to advocate for Kowalski's
finite semantic trees because they carry a visual representation of
Herbrand (equality) interpretations that helps the intuition. We show
that very different strategies can be shown complete by using this
method: ordered resolution, ordered resolution with selection, linear
resolution, and ordered resolution and paramodulation. These
strategies had not been proved complete before by means of finite
semantic trees, including the first and the last ones proved complete
by Rusinowitch and Hsiang with transfinite semantic trees. Using
finite semantic trees happened to be an interesting technical
challenge in all cases but the first. A first important lesson we
learned is that the concepts elaborated by Ganzinger and his
collaborators are intrinsic to the entire field of automated
deduction, rather than specific to his model generation proof method
as one might have thought. A second is that semantic trees are
flexible and powerful enough to challenge Bachmair and Ganzinger
method. However, are both methods really different ?
full paper