ProTeM: a proof term manipulator (system description)

DOI10.4230/LIPICS.FSCD.2018.31MaRDI QIDQ4993363zbMATH OpenFDO

Authors Christina Kohl, Aart Middeldorp

Publication date 15 June 2021

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2018.31

zbMATH Keywords

interactive toolproof termsterm 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 4078854
• Certifying term rewriting proofs in ELAN
• Tyrolean termination tool: techniques and features
• scientific article; zbMATH DE number 2043537
• scientific article; zbMATH DE number 3902026

Cites work

• Certification of classical confluence results for left-linear term rewrite systems
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Decreasing diagrams and relative termination
• Developing developments
• Four equivalent equivalences of reductions
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• Proof Terms for Infinitary Rewriting

Cited in

(4)

• Composing proof terms
• Quati: an automated tool for proving permutation lemmas
• scientific article; zbMATH DE number 4078854 (Why is no real title available?)
• System Description: The Proof Transformation System CERES

Describes a project that uses

Uses Software

• TPDB
• ProTeM

This page was built for publication: ProTeM: a proof term manipulator (system description)

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