How to Prove Ground Confluence
- We show how to prove ground confluence of term rewrite relations that areinduced by reductive systems of clausal rewrite rules. According to a well-knowncritical pair criterion it suffices for such systems to prove ground joinability ofa suitable set of 'critical clauses'. We outline how the latter can be done in asystematic fashion, using mathematical induction as a key concept of reasoning.
Download full text files
Additional Services
| Author: | Klaus Becker |
|---|---|
| URN: | urn:nbn:de:hbz:386-kluedo-3590 |
| Series (Serial Number): | SEKI Report (96,2) |
| 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 |
| 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 |