Paper Description: MIP-9401

BibTeX entry:

@incollection{MIP-9401,
author="U. Fraus",
title="Inductive Theorem Proving for Algebraic Specifications TIP System User's Manual",
institution="Fakult{\"a}t f{\"u}r Mathematik und Informatik, Universit{\"a}t Passau",
year=1994,
number={MIP-9401}
}

Abstract:

This manual introduces an inductive theorem prover called TIP system (Term Induction Prover). This prover can be used to verify universally quantified systems of conditional equations over algebraic specifications. The proofs can be done in either an interactive or an automatic way. The reader learns how to use the TIP system, especially how to do inductive proofs in an interactive way. Besides, the internal proof algorithm and the built-in heuristics are explained and some useful techniques for successful theorem proving are presented.

Paper itself:

Cross links:

Ulrike Peiker, Martin Griebl