A New and Formalized Proof of Abstract Completion

DOI10.1007/978-3-319-08970-6_19MaRDI QIDQ2879259zbMATH OpenOpenAlexFDO

Authors Nao Hirokawa, Aart Middeldorp, Christian Sternagel

Publication date 8 September 2014

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08970-6_19

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Abstract completion, formalized
• Completeness of Proof Systems for Equational Specifications
• Completeness in Proof-Theoretic Semantics
• scientific article; zbMATH DE number 4049135
• Some experiments with a completion theorem prover
• Abstractions of uniform proofs
• scientific article; zbMATH DE number 3900184
• Abstract proof checking: An example motivated by an incompleteness theorem
• scientific article; zbMATH DE number 2219536

Cited in

(6)

• Completion for logically constrained rewriting
• scientific article; zbMATH DE number 7204438 (Why is no real title available?)
• Abstract completion, formalized
• Completion Is an Instance of Abstract Canonical System Inference
• Proof transformation for non-compatible rewriting
• An Iabelle/HOL formalization of narrowing and multiset narrowing for E-unifiability, reachability and infeasibility

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

This page was built for publication: A New and Formalized Proof of Abstract Completion

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