A PVS Theory for Term Rewriting Systems

DOI10.1016/j.entcs.2009.07.049zbMath1310.68124OpenAlexW2025817323WikidataQ58001452 ScholiaQ58001452MaRDI QIDQ5178962

André L. Galdino, Mauricio Ayala-Rincón

Publication date: 18 March 2015

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.07.049

zbMATH Keywords

term rewriting systemsabstract reduction systemsPVSformalization of theorems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)

Related Items (2)

A formalization of the Knuth-Bendix(-Huet) critical pair theorem ⋮ Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem

Uses Software

• Isabelle/HOL
• PVS
• NQTHM
• CoLoR
• SAEPTUM
• FELIX
• RRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• More Church-Rosser proofs (in Isabelle/HOL)
• Formal proofs about rewriting using ACL2
• Types for proofs and programs. International Workshop TYPES '94, Båstad, Sweden, June 6-10, 1994. Selected papers
• Some lambda calculus and type theory formalized
• Certification of Automated Termination Proofs
• A mechanical proof of the Church-Rosser theorem
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Development closed critical pairs
• Residual theory in λ-calculus: a formal development

This page was built for publication: A PVS Theory for Term Rewriting Systems