Computational aspects of an order-sorted logic with term declarations (Q1801289)

The order-sorted logic is a kind of many-sorted logic with sorts being partially ordered and substitutions of terms belonging to subsorts instead of variables of a given sort allowed (e.g. substitutions of natural numbers instead of integers, rationals, reals, etc. are valid). The book under review being the revised and edited version of the author's Ph.D. Thesis (1988) is devoted to the investigation of order- sorted logic, its proof-theoretic and computational aspects. The book consists of the introductory chapter giving motivations, describing related work, presenting an overview, and five parts. Part I of the book gives an account of order-sorted logic, its algebraic treatment and semantics. Birkhoff's theorem for equational logic is extended to order-sorted algebras, a rule-based approach to unification in Martelli-Montanari's style is developed. In Part II the distinctions and similarities between well-sorted and ill- sorted terms are investigated. The general conditions for term rewriting system to be sort-compatible and canonical are worked out, and a completion procedure for ground term rewriting systems is described. Several equivalent formulations for a sorted signature with term declarations are introduced. The Herbrand theorem in the context of sorts and equations is proved. Parts III and IV of the book are devoted to unification algorithms, both for uninterpreted and interpreted (by means of equational theories) order-sorted terms. It is shown that unification in elementary regular signatures is decidable, finitary, and generaly unification is undecidable, may be infinitary, but minimal sets of unifiers always exist and are recursively enumerable. The complexity of unification for different types of signatures is investigated. In the case of interpreted terms, satisfying a set of equational axioms, a complete rule-based sorted unification procedure is given. In Part V a complete resolution- based calculus with a sorted unification algorithm is described and validated. The completeness of resolution with paramodulation provide a refutationally complete calculus for equality if the functionally reflexive axioms are in the clause set. The proof follows the usual guidelines, including Herbrand's theorem and lifting arguments. An alternative to paramodulation, the E-resolution is discussed. This book is primarily aimed at researches in the field of automated theorem proving and logic programming. All these researchers will appreciate the insight and technical flair displayed by the author.