Computational aspects of an order-sorted logic with term declarations
type: Item
instance of: scholarly article
title: Computational aspects of an order-sorted logic with term declarations
zbMATH Open document ID: 0689.68001
author: Manfred Schmidt-Schauß
published in: Lecture Notes in Computer Science
publication date: 1993-06-05T00:00:00Z
review text: 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 describe…
Mathematics Subject Classification ID: 68-02
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03D03
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 195008
zbMATH Keywords: equational theory
zbMATH Keywords: unification
zbMATH Keywords: term rewriting system
zbMATH Keywords: resolution
zbMATH Keywords: paramodulation
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 195008