Proving and rewriting

DOI10.1007/3-540-53162-9_27MaRDI QIDQ5096184zbMATH OpenOpenAlexFDO

Authors Joseph 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

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

Recommendations

• Term rewriting and beyond -- theorem proving in Isabelle
• scientific article; zbMATH DE number 4074536
• Refutational theorem proving using term-rewriting systems
• scientific article; zbMATH DE number 785049
• Proving geometry theorems with rewrite rules

Cites work

• A framework for defining logics
• Completeness of Proof Systems for Equational Specifications
• scientific article; zbMATH DE number 3821084 (Why is no real title available?)
• scientific article; zbMATH DE number 3911679 (Why is no real title available?)
• scientific article; zbMATH DE number 3949706 (Why is no real title available?)
• scientific article; zbMATH DE number 3991418 (Why is no real title available?)
• scientific article; zbMATH DE number 4060701 (Why is no real title available?)
• scientific article; zbMATH DE number 4074535 (Why is no real title available?)
• scientific article; zbMATH DE number 4090765 (Why is no real title available?)
• scientific article; zbMATH DE number 4090779 (Why is no real title available?)
• scientific article; zbMATH DE number 3684925 (Why is no real title available?)
• scientific article; zbMATH DE number 3997131 (Why is no real title available?)
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Proving Properties of Programs by Structural Induction
• The foundation of a generic theorem prover

Cited in

(15)

• Proving geometry theorems with rewrite rules
• Category-based modularisation for equational logic programming
• On rewriting rules in Mizar
• Soundness in verification of algebraic specifications with OBJ
• Verifying an infinite systolic algorithm using third-order equational methods
• Rewriting Induction + Linear Arithmetic = Decision Procedure
• scientific article; zbMATH DE number 4074536 (Why is no real title available?)
• scientific article; zbMATH DE number 88983 (Why is no real title available?)
• A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler
• Automata, Languages and Programming
• Proof search and proof check for equational and inductive theorems.
• Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
• NuITP: accelerating the inductive verification of equational programs through symbolic simplification
• A higher-order implementation of rewriting
• Term rewriting and beyond -- theorem proving in Isabelle

This page was built for publication: Proving and rewriting

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