Observational proofs by rewriting.
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 3888893 (Why is no real title available?)
- scientific article; zbMATH DE number 3812932 (Why is no real title available?)
- scientific article; zbMATH DE number 3898213 (Why is no real title available?)
- scientific article; zbMATH DE number 3945335 (Why is no real title available?)
- scientific article; zbMATH DE number 193539 (Why is no real title available?)
- scientific article; zbMATH DE number 1231661 (Why is no real title available?)
- scientific article; zbMATH DE number 1988979 (Why is no real title available?)
- scientific article; zbMATH DE number 1761887 (Why is no real title available?)
- scientific article; zbMATH DE number 4113952 (Why is no real title available?)
- scientific article; zbMATH DE number 1418819 (Why is no real title available?)
- Automated theorem proving by test set induction
- Automating inductionless induction using test sets
- Behavioural approaches to algebraic specifications. A comparative study
- Behavioural theories and the proof of behavioural properties
- Context induction: A proof principle for behavioural abstractions and algebraic implementations
- Encompassment properties and automata with constraints
- Extending Bachmair's method for proof by consistency to the final algebra
- Final algebra semantics and data type extensions
- Implementing contextual rewriting
- Implicit induction in conditional theories
- Testing for the ground (co-)reducibility property in term-rewriting systems
- Theorem-proving with resolution and superposition
- Toward formal development of programs from algebraic specifications: Implementations revisited
Cited in
(10)- Formal design and verification of operational transformation algorithms for copies convergence
- Using induction and rewriting to verify and complete parameterized specifications
- scientific article; zbMATH DE number 2038889 (Why is no real title available?)
- 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)
