Proving and rewriting

DOI10.1007/3-540-53162-9_27zbMath1496.03045OpenAlexW1792334848MaRDI QIDQ5096184

Joseph A. Goguen

Publication date: 16 August 2022

Published in: Algebraic and Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-53162-9_27

Mathematics Subject Classification ID

Applications of universal algebra in computer science (08A70) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler ⋮ Category-based modularisation for equational logic programming ⋮ Soundness in verification of algebraic specifications with OBJ ⋮ Verifying an infinite systolic algorithm using third-order equational methods

Cites Work

• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• The foundation of a generic theorem prover
• Completeness of Proof Systems for Equational Specifications
• A framework for defining logics
• Proving Properties of Programs by Structural Induction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item