A many-sorted calculus based on resolution and paramodulation. (English) Zbl 0669.68059

Research Notes in Artificial Intelligence. London: Pitman Publishing; Los Altos, CA: Morgan Kaufmann Publ., Inc. 160 p. £17.95 (1987).
A many-sorted calculus based on resolution and paramodulation is introduced (many-sorted language, semantics, modified rules). Theorem proving within this calculus is presented. The ground completeness, a version of the unification theorem, the completeness and the Sort-Theorem is proved for the many-sorted calculus.
In comparison with the unsorted calculus for the many-sorted calculus a more efficient deduction is obtained which avoids useless conclusions (drastic reduction of the search space, shorter refutations of smaller sets of shorter clauses).
Reviewer: E.Melis


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
68-02 Research exposition (monographs, survey articles) pertaining to computer science
03B10 Classical first-order logic