TRS: Term Rewriting and Abstract Reduction Systems Theories
For PVS 6.0
André Luiz Galdino
Universidade de Brasília &
Campus Catalão/Universidade Federal de Goiás
Brazil
[email protected]
Mauricio Ayala Rincón
Universidade de Brasília
Brazil
[email protected]
Contains a unification theory developed by both authors together with
Andréia Borges Avelar
Universidade de Brasília
Brazil
[email protected]
orthogonality: Formalizes confluence of orhtogonal TRSs importing the
PVS theory for Term Rewriting and Abstract Reduction Systems trs
available at NASA LaRC PVS libraries. This formalization follows
closely analytical proofs as the one presented in Baader & Nipkow's
famous textbook "Term Rewriting and All That" and uses the
Parallel Moves Lemma.
Last update: 24 May, 2013
Ana Cristina Rocha Oliveira,
Mauricio Ayala-Rincon &
André Luiz Galdino
Grupo de Teoria da Computacao
Universidade de Brasília
[email protected]
[email protected]
[email protected]
1. Package Files
----------------
a. README Summary of distribution (this file)
b. This library contains the ARS, TRS, and orthogonality 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.
orthogonality theory
--------------------
orthogonality.pvs contains definitions and formalizations. A few basic
ones are related with parallel reduction relation.
orthogonality.prf contains the formalization per se.
2. REQUIREMENTS
---------------
a. Make sure PVS 6.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.
------------------------
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
