• search hit 1 of 1
Back to Result List

Guiding equational proofs by attribute functions

  • This report presents a methodology to guide equational reasoningin a goal directed way. Suggested by rippling methods developed inthe field of inductive theorem proving we use attributes of terms andheuristics to determine bridge lemmas, i.e. lemmas which have tobe used during the proof of the theorem. Once we have found sucha bridge lemma we use the techniques of difference unification andrippling to enable its use.

Download full text files

Export metadata

Additional Services

Search Google Scholar
Metadaten
Author:Jürgen Cleve, Dieter Hutter
URN:urn:nbn:de:hbz:386-kluedo-3254
Series (Serial Number):SEKI Report (93,15)
Document Type:Preprint
Language of publication:English
Year of Completion:1999
Year of first Publication:1999
Publishing Institution:Technische Universität Kaiserslautern
Date of the Publication (Server):2000/04/03
Tag:Automated Reasoning; Deduction; Difference Reduction; Equational Reasoning
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011