Composing proof terms

DOI10.1007/978-3-030-29436-6_20MaRDI QIDQ2305425zbMATH OpenOpenAlexFDO

Authors Christina Kohl, Aart Middeldorp

Publication date 10 March 2020

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-29436-6_20

zbMATH Keywords

automationterm rewritingproof terms

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• ProTeM: a proof term manipulator (system description)
• Proof Terms for Infinitary Rewriting
• scientific article; zbMATH DE number 785049
• Compositional term rewriting: An algebraic proof of Toyama's theorem
• Projections for infinitary rewriting (extended version)

Cites work

• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 794240 (Why is no real title available?)
• Conditional rewriting logic as a unified model of concurrency
• Decreasing diagrams and relative termination
• Four equivalent equivalences of reductions
• ProTeM: a proof term manipulator (system description)
• Rewriting logic: Roadmap and bibliography
• Term Rewriting and All That

Cited in

(1)

• ProTeM

This page was built for publication: Composing proof terms

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