scientific article; zbMATH DE number 7204438

DOI10.4230/LIPICS.FSCD.2017.19zbMATH Open1441.68113MaRDI QIDQ5111315FDOQ5111315

Sarah Winkler, Nao Hirokawa, Aart Middeldorp, Christian Sternagel

Publication date: 26 May 2020

Title of this publication is not available (Why is that?)

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

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)

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Term Rewriting and All That
• Title not available (Why is that?)
• Title not available (Why is that?)
• About the rewriting systems produced by the Knuth-Bendix completion algorithm
• Title not available (Why is that?)
• Title not available (Why is that?)
• Confluence by Decreasing Diagrams
• A finite Thue system with decidable word problem and without equivalent finite canonical system
• Title not available (Why is that?)
• Title not available (Why is that?)
• On interreduction of semi-complete term rewriting systems
• Syntactical methods for braids of three strands
• Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
• A New and Formalized Proof of Abstract Completion

Cited In (5)

• Extending Maximal Completion (Invited Talk)
• On proving properties of completion strategies
• Verified Given Clause Procedures
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Certified equational reasoning via ordered completion

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

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)