A few exercises in theorem processing

DOI10.1016/J.TCS.2006.12.037MaRDI QIDQ879370zbMATH OpenOpenAlexFDO

Authors F. L. Morris

Publication date 11 May 2007

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2006.12.037

zbMATH Keywords

conversionsderived inference ruleslist processingtheorem processing

Mathematics Subject Classification ID

Recommendations

• Lessons learned from LCF: A Survey of Natural Deduction Proofs
• scientific article; zbMATH DE number 1670733
• scientific article; zbMATH DE number 2185700
• A higher-order implementation of rewriting
• Term rewriting and beyond -- theorem proving in Isabelle

Cites work

• scientific article; zbMATH DE number 1259143 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 958048 (Why is no real title available?)
• A higher-order implementation of rewriting
• Edinburgh LCF. A mechanized logic of computation
• GEDANKEN—a simple typeless language based on the principle of completeness and the reference concept

Cited in

(4)

• scientific article; zbMATH DE number 2185700 (Why is no real title available?)
• Fix your types
• Lessons learned from LCF: A Survey of Natural Deduction Proofs
• scientific article; zbMATH DE number 1670733 (Why is no real title available?)

Describes a project that uses

Uses Software

• HOL
• ML

This page was built for publication: A few exercises in theorem processing

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