de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

Unification in sort theories and its applications

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45719

Weidenbach,  Christoph
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)

MPI-I-93-211.pdf
(Any fulltext), 183KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Weidenbach, C.(1993). Unification in sort theories and its applications (MPI-I-93-211). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-B43E-D
Abstract
In this article I investigate the properties of unification in sort theories. The usual notion of a sort consisting of a sort symbol is extended to a set of sort symbols. In this language sorted unification in elementary sort theories is of unification type finitary. The rules of standard unification with the addition of four sorted rules form the new sorted unification algorithm. The algorithm is proved sound and complete. The rule based form of the algorithm is not suitable for an implementation because there is no control and the used data structures are weak. Therefore we transform the algorithm into a deterministic sorted unification procedure. For the procedure sorted unification in pseudo-linear sort theories is proved decidable. The notions of a sort and a sort theory are developed in a way such that a standard calculus can be turned into a sorted calculus by replacing standard unification with sorted unification. To this end sorts may denote the empty set. Sort theories may contain clauses with more than one declaration and may change dynamically during the deduction process. The applicability of the approach is exemplified for the resolution and the tableau calculus.