Teaching Higher-Order Logic Using Isabelle

要約

私たちは、基本的なフレームワーク Isabelle/Pure に直接構築され、可能な限り小さくて読みやすいように開発された Isabelle 証明アシスタントの高次ロジックの形式化を提示します。
したがって、これは、より高度な自動化を備えたより複雑な Isabelle/HOL を学習することなく、高次のロジックと証明アシスタントについて学習しようとしている人にとって、良い入門として役立つはずです。
私たちの開発とアプローチを紹介するために、サンプル証明を説明し、高次論理の公理と規則を説明し、教室でこの主題を教えた経験について話し合います。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google