# Author: Robert Staerk # Created: Tue Oct 12 18:09:53 1993 # Filename: semiunify.README This is an efficient general semiunification algorithm implemented in C. The algorithm is part of the project 'Semiunification and most general induction proofs' of Hans Leiss. A semiunification problem is a finite set S of equations of the form s = t or inequations of the form s <=_i t, where s and t are terms and 1 <= i <= n for some natural number n. A solution of S is an (n+1)-tuple of substitutions (sigma,tau_1,...,tau_n) such that (1) for any equation s = t of S: s sigma = t sigma, (2) for any inequation s <=_i t of S: s sigma tau_i = t sigma. In contrast to unification the semiunification problem is not decidable. If a semiunification problem has a solution then our implementation will compute the most general solution. Our implementation will also recognize some unsolvable problems. Since the semiunfication problem is not decidable, however, there must exist input problems such that our algorithm diverges. The archive semiunify-1.0.tar contains the following files and directories: semiunify-1.0/README semiunify-1.0/INSTALLATION semiunify-1.0/USERMANUAL semiunify-1.0/src semiunify-1.0/test The src directory contains a detailed description of the algorithm and a correctness proof. The test directory contains examples. ---------------------------------------------------------------------- Robert F. St"ark | Phone: +49 89 2394 44 62 Mathematisches Institut | Fax: +49 89 2805 248 Universit"at M"unchen | Email: staerk@rz.mathematik.uni-muenchen.de Theresienstrasse 39 | Room 337 D-80333 M"unchen | ----------------------------------------------------------------------