Teaching Higher-Order Logic Using Isabelle
Electronic Proceedings in Theoretical Computer Science(2024)
摘要
We present a formalization of higher-order logic in the Isabelle proof
assistant, building directly on the foundational framework Isabelle/Pure and
developed to be as small and readable as possible. It should therefore serve as
a good introduction for someone looking into learning about higher-order logic
and proof assistants, without having to study the much more complex
Isabelle/HOL with heavier automation. To showcase our development and approach
we explain a sample proof, describe the axioms and rules of our higher-order
logic, and discuss our experience with teaching the subject in a classroom
setting.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要