This work presents a theorem prover for inductive proofs within an equational theory which supports the verification of universally quantified equations. This system, called TIP, is based on a modification of the well-known narrowing algorithm. Particulars of the implementation are stated and practical experiences are summarized.
CITATION STYLE
Fraus, U., & Hußmann, H. (1991). A narrowing-based theorem prover. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 528 LNCS, pp. 421–422). Springer Verlag. https://doi.org/10.1007/3-540-54444-5_118
Mendeley helps you to discover research relevant for your work.