Contextual rewriting as a sound and complete proof method for conditional LOG-specifications

DOI10.1007/BF01178578zbMath0790.68075OpenAlexW2080171448MaRDI QIDQ1323311

Fernando Orejas, Marisa Navarro, Jean-Luc Rémy

Publication date: 10 May 1994

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01178578

zbMATH Keywords

terminationalgebraic specificationconditional specifications with predicatescontextual rewritingproof-system

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Grammars and rewriting systems (68Q42)

Uses Software

• REVE

Cites Work

• Canonical constraints for parameterized data types
• Conditional rewrite rules
• Conditional rewrite rules: Confluence and termination
• Completeness of calculii for axiomatically defined classes of algebras
• Data Type Specification: Parameterization and the Power of Specification Techniques
• Equality, types, modules, and (why not?) generics for logic programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Contextual rewriting as a sound and complete proof method for conditional LOG-specifications