Abstract completion, formalized

MaRDI QIDQ5232901zbMATH OpenFDO

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

Publication date 13 September 2019

Full work available at URL https://arxiv.org/abs/1802.08437

zbMATH Keywords

abstract completioncanonicityIsabelle/HOLordered completionterm rewriting

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 7204438
• A New and Formalized Proof of Abstract Completion
• Completion Is an Instance of Abstract Canonical System Inference
• Completion for logically constrained rewriting
• Formalizing Knuth-Bendix orders and Knuth-Bendix completion

Cited in

(13)

• Certified equational reasoning via ordered completion
• A New and Formalized Proof of Abstract Completion
• Completion for logically constrained rewriting
• On proving properties of completion strategies
• scientific article; zbMATH DE number 7204438 (Why is no real title available?)
• Abstract canonical inference
• Completion Is an Instance of Abstract Canonical System Inference
• Observational Completeness on Abstract Interpretation
• Order Reconfiguration under Width Constraints
• Left-Linear Completion with AC Axioms
• Proof transformation for non-compatible rewriting
• The computability path order for beta-eta-normal higher-order rewriting
• Left-linear completion with AC axioms

Describes a project that uses

Uses Software

• Isabelle/HOL
• CeTA
• CiME

This page was built for publication: Abstract completion, formalized

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