scientific article; zbMATH DE number 7204438

DOI10.4230/LIPICS.FSCD.2017.19MaRDI QIDQ5111315zbMATH OpenFDO

Authors Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler

Publication date 26 May 2020

zbMATH Keywords

term rewritingIsabelle/HOLcanonicityordered completionabstract completion

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Abstract completion, formalized
• A New and Formalized Proof of Abstract Completion
• Completion Is an Instance of Abstract Canonical System Inference
• Completion for logically constrained rewriting
• Completion procedures as semidecision procedures

Cites work

• scientific article; zbMATH DE number 3981150 (Why is no real title available?)
• scientific article; zbMATH DE number 4047065 (Why is no real title available?)
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 50648 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• A New and Formalized Proof of Abstract Completion
• A finite Thue system with decidable word problem and without equivalent finite canonical system
• About the rewriting systems produced by the Knuth-Bendix completion algorithm
• Confluence by Decreasing Diagrams
• Formalizing Knuth-Bendix orders and Knuth-Bendix completion
• Isabelle/HOL. A proof assistant for higher-order logic
• On interreduction of semi-complete term rewriting systems
• Syntactical methods for braids of three strands
• Term Rewriting and All That

Cited in

(8)

• Proof transformation for non-compatible rewriting
• Extending Maximal Completion (Invited Talk)
• Formalized proofs of the infinity and normal form predicates in the first-order theory of rewriting
• On proving properties of completion strategies
• Verified Given Clause Procedures
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Abstract completion, formalized
• Certified equational reasoning via ordered completion

Describes a project that uses

Uses Software

• HOL
• Isabelle/HOL
• Isabelle

This page was built for publication:

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