A Guide to UNICOM, an Inductive Theorem Prover Based on Rewriting
and Completion Techniques

Bernhard Gramlich, Wolfgang Lindner
Fachbereich Informatik, Universitaet Kaiserslautern
D-67653 Kaiserslautern, Germany
E-mail: gramlich@informatik.uni-kl.de

Abstract
We provide an overview of UNICOM, an inductive theorem prover
for equational logic which is based on refined rewriting and
completion techniques. The architecture of the system as well
as its functionality are described. Moreover, an insight into the
most important aspects of the internal proof process is provided.
This knowledge about how the central inductive proof component of
the system essentially works is crucial for human users
who want to solve non-trivial proof tasks with UNICOM and thoroughly
analyse potential failures. The presentation is focussed
on practical aspects of understanding and using UNICOM.
A brief but complete description of the
command interface, an installation guide, an example session, a
detailed extended example illustrating various special features
and a collection of successfully handled examples are also included.

Key Words
inductive theorem proving, term rewriting systems, completion
techniques

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1991/papers
file: Lindner.SR-91-17.ps.gz