A Guide to UNICOM, an Inductive Theorem Prover Based on Rewriting and Completion Techniques
Bernhard Gramlich, Wolfgang F. Lindner · 1999
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. This work was supported by the 'Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt)'. Contents 1 Introduction and Overview 4 2 The User...