Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification

DOI10.1007/978-3-030-63595-4_7MaRDI QIDQ6486039zbMATH OpenFDO

Authors José Meseguer, Stephen Skeirik

Publication date 22 December 2022

Published in 1517.68167 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-63595-4_7

Mathematics Subject Classification ID

Logic in computer science (03B70) Grammars and rewriting systems (68Q42)

Recommendations

• Automatic proofs by induction in theories without constructors
• Proofs by induction in equational theories with constructors
• Inductive proofs by specification transformations
• scientific article; zbMATH DE number 177848
• Equational formulae with membership constraints

Cited in

(7)

• Equational formulae with membership constraints
• Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
• Checking Sufficient Completeness by Inductive Theorem Proving
• On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
• Building correct-by-construction systems with formal patterns
• Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
• NuITP: accelerating the inductive verification of equational programs through symbolic simplification

This page was built for publication: Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification

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