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