A few exercises in theorem processing

DOI10.1016/J.TCS.2006.12.037zbMATH Open1111.68114OpenAlexW2067501613MaRDI QIDQ879370FDOQ879370

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

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

zbMATH Keywords

conversionsderived inference ruleslist processingtheorem processing

Mathematics Subject Classification ID

Cites Work

• Title not available (Why is that?)
• Edinburgh LCF. A mechanized logic of computation
• Title not available (Why is that?)
• Title not available (Why is that?)
• A higher-order implementation of rewriting
• GEDANKEN—a simple typeless language based on the principle of completeness and the reference concept

Cited In (4)

• Fix your types
• Title not available (Why is that?)
• Lessons learned from LCF: A Survey of Natural Deduction Proofs
• Title not available (Why is that?)

Uses Software

• ML
• HOL

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)