07.06.2016
Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System
Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2017
EinloggenAktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstract
orthogonality
inside the directory TRS
of the NASA Langley PVS Library. Like all of TRS
, orthogonality
is intended to stay close to textbook proofs. The present proof uses the Parallel Moves Lemma at dominating positions of a parallel context. In this manner, all parallel forks filling the holes of the context are joined and, as result, a term of joinability for the whole fork is constructed.