A New and Formalized Proof of Abstract Completion

DOI10.1007/978-3-319-08970-6_19zbMATH Open1416.68164OpenAlexW1588278029MaRDI QIDQ2879259FDOQ2879259

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

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

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cited In (5)

• Proof transformation for non-compatible rewriting
• Completion Is an Instance of Abstract Canonical System Inference
• Title not available (Why is that?)
• Abstract completion, formalized
• Completion for logically constrained rewriting

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)