| products/sources/formale Sprachen/PVS/TRS/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: README Sprache: SMLOriginal von: PVS© |
|
||||||
|
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.0 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.Bot Zugriff |
