Theorem Proving in Higher Order Logics

DOI10.1007/B100400zbMATH Open1099.68727OpenAlexW2798038182MaRDI QIDQ5464643FDOQ5464643

Authors Jason Hickey, Aleksey Nogin

Publication date 18 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b100400

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1670747
• Implementing tactics and tacticals in a higher-order logic programming language
• A Proof-Theoretic Approach to Tactics
• Tactics and parameters
• Metalogical frameworks. II: Developing a reflected decision procedure

Cited in

(9)

• Tactics for hierarchical proof
• Improving the Usability of HOL Through Controlled Automation Tactics
• scientific article; zbMATH DE number 1670747 (Why is no real title available?)
• Formal compiler construction in a logical framework
• Implementing tactics and tacticals in a higher-order logic programming language
• A calculus of tactics and its operational semantics
• Tactics and parameters
• scientific article; zbMATH DE number 3870643 (Why is no real title available?)
• Reflection of formal tactics in a deductive reflection framework

Describes a project that uses

Uses Software

• MetaPRL
• OCaml

This page was built for publication: Theorem Proving in Higher Order Logics

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