Observational proofs by rewriting.

DOI10.1016/S0304-3975(01)00333-4zbMath1051.68085MaRDI QIDQ1607227

Adel Bouhoula, Michaël Rusinowitch

Publication date: 31 July 2002

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

zbMATH Keywords

InductionRewritingAutomated proofsObservational semantics

Mathematics Subject Classification ID

Related Items (8)

Formal design and verification of operational transformation algorithms for copies convergence ⋮ Closure properties for the class of behavioral models ⋮ Behavioral equivalence of hidden \(k\)-logics: an abstract algebraic approach ⋮ A short overview of Hidden Logic ⋮ Observational Refinement Process ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ Behavioural reasoning for conditional equations ⋮ Towards Behavioral Maude

Cites Work

• Behavioural theories and the proof of behavioural properties
• Testing for the ground (co-)reducibility property in term-rewriting systems
• Theorem-proving with resolution and superposition
• Automating inductionless induction using test sets
• Toward formal development of programs from algebraic specifications: Implementations revisited
• Final algebra semantics and data type extensions
• Context induction: A proof principle for behavioural abstractions and algebraic implementations
• Extending Bachmair's method for proof by consistency to the final algebra
• Behavioural approaches to algebraic specifications. A comparative study
• Automated theorem proving by test set induction
• Implicit induction in conditional theories
• Encompassment properties and automata with constraints
• Implementing contextual rewriting
• 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: Observational proofs by rewriting.