Quelle  README   Sprache: Text

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
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

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 

anacrismarie@gmail.com
galdino@catalao.ufg.br
ayala@unb.br

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.

------------------------