TRS: Term Rewriting and Abstract Reduction Systems Theories
For PVS 5.0
André Luiz Galdino
Universidade de Brasília &
Campus Catalão/Universidade Federal de Goiás
Brazil
galdino@catalao.ufg.br
Mauricio Ayala Rincón
Universidade de Brasília
Brazil
ayala@unb.br
Contains a unification theory developed by both authors together with
Andréia Borges Avelar
Universidade de Brasília
Brazil
avelarab@gmail.com
1. Package Files
----------------
a. README Summary of distribution (this file)
b. The folder "trs-pvs50" which contains the ARS and TRS theories
-------------------------------------------------------------------
b.1. ARS theories
-----------------
relations_closure.pvs This theory contains the definitions of closure
of a relation and some properties.
ars_terminology.pvs This theory contains some terminology of ARS such
as unique normal form, reducible and sucessor, and
notions of confluence and commutation.
results_confluence.pvs This theory contains some results about confluence
such as strong confluent implies semi-confluent.
results_commutation.pvs This theory contains some results about commutation
such as Commutation lemma.
results_normal_form.pvs This theory contains some results involving normal
form such as a relation is normalizing and
confluent iff every element has a unique
normal form.
noetherian.pvs This theory contains the definition of convergent
reduction and noetherian relation and the
Noetherian induction lemma.
newman_yokouchi.pvs This theory contains the specification of Newman's
lemma and Yokouchi's lemma
modulo_equivalence.pvs This theory contains specifications about Reduction
modulo equivalence such as local confluence, confluence
and Church-Rosser property modulo equivalence, and some
properties such as the general newman's lemma.
confluence_commute.pvs This theory contains some results and exercises from
the book TeReSe.
b.2. TRS theories
-----------------
arity.pvs This theory contains the definition of the function
arity.
term.pvs This theory contain the definition of an abstract term
structure.
variables_term.pvs This theory contain the definition of a variable set V.
term_adt.pvs This theory is automatically generated by the
specification of a term (term.pvs) and contains
extensionality axioms, eta axiom, induction scheme and
a well-foundedness axiom.
positions.pvs This theory contains the definitons of the set of
positions of a term, parallel positions among other,
and some properties of positions.
subterm.pvs This theory contains the notions of subterm of a term,
and variables occurring in a term, and some properties.
replacement.pvs This theory contains the definition of replacing the
subterm at some position by a term, and some properties.
compatibility.pvs This theory contains the definitions of closed under
substitutions and operations, and compatible with
operations and contexts, and some properties such as
compatible with operations iff compatible with contexts.
substitution.pvs This theory contains the definitions of substitution,
domain and range of a substitution, restriction and
extention of a substitution, composition of two
substitutions, and a most general unifier,
and some properties.
extending_rename.pvs This theory contain the definition that extend a rename
from a given domain to the same type as identity.
rewrite_rules.pvs This theory contains the definitions of a rewrite rule
and a set (type) of rewrite rules.
reduction.pvs This theory contains the definition of reduction
relations and some properties such as closed under
substitutions and compatible with operations.
replace_positions.pvs This theory contain the notion of substitutes all subterms
at a sequence of parallel positions of a term by another term,
and some properties.
unification.pvs This theory is composed of a set of specifications and
formalization of definitions and lemmas which allowed us
to formalize the lemma which guarantee the existence of a most
general unifier on set first-order terms.
robinsonunification.pvs This theory contains the formalization of a greedy first-order
unification algorithm a la Robinson.
robinsonunificationEF.pvs This theory contains the formalization of a more efficient
first-order unification algorithm a la Robinson.
critical_pairs_aux.pvs This theory contains definitions and properties needful to
prove the Critical Pairs Theorem.
critical_pairs.pvs This theory contains the definition of a Critical Pairs
and the Critical Pairs Theorem.
finite_sequences_extras.pvs This theory contains definitions and properties about
finite sequences.
IUnion_extra.pvs This theory contains aditional properties about disjoint
sets operations and finite union of a finite family of
finite sets.
PVS-STATUS_top This file contains the Proof summary for ars, trs, unification,
robinsonunification, and robinsonunificationEF theories generated
using the proof command prove-importchain from the theory trs.
2. REQUIREMENTS
---------------
a. Make sure PVS 5.0 has been installed.
Available at: http://pvs.csl.sri.com/
b. trs theory requires NASA Langley PVS Libraries which are available at:
http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html
These libraries should be included.
------------------------