Observational proofs by rewriting.

DOI10.1016/S0304-3975(01)00333-4zbMATH Open1051.68085MaRDI QIDQ1607227FDOQ1607227

Authors: Adel Bouhoula, Michaël Rusinowitch 

Publication date: 31 July 2002

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

Recommendations

• scientific article; zbMATH DE number 2038889
• Observational implementations
• scientific article; zbMATH DE number 785047
• Constructor-based observational logic
• Observational specifications and the indistinguishability assumption

zbMATH Keywords

RewritingAutomated proofsInductionObservational semantics

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

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

Cited In (10)

• Formal design and verification of operational transformation algorithms for copies convergence
• Using induction and rewriting to verify and complete parameterized specifications
• Title not available (Why is that?)
• Behavioral equivalence of hidden \(k\)-logics: an abstract algebraic approach
• A short overview of hidden logic
• Behavioural reasoning for conditional equations
• Observational refinement process
• Towards behavioral Maude: behavioral membership equational logic
• Closure properties for the class of behavioral models
• Mechanically certifying formula-based Noetherian induction reasoning

This page was built for publication: Observational proofs by rewriting.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1607227)