Theorem Proving in Dependently-Typed Higher-Order Logic — Extended Preprint

要約

高次ロジック HOL は、型付きデータ構造を表現および推論するための非常に単純な構文とセマンティクスを提供します。
しかし、その型システムには、型が用語に依存する可能性がある高度な機能がありません。
依存型理論はこのような豊富な型システムを提供しますが、HOL とはかなり概念的な違いがあり、証明の自動化サポートも比較的貧弱です。
HOL のスタイルと概念フレームワークを保持する、HOL の依存型拡張 DHOL を導入します。
さらに、DHOL から HOL への変換を構築し、それを HOL 定理証明器へのプリプロセッサとして実装することで、DHOL 用の定理証明器を取得します。

要約(オリジナル)

Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a rich type system, but has rather substantial conceptual differences to HOL, as well as comparatively poor proof automation support. We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to a HOL theorem prover, thereby obtaining a theorem prover for DHOL.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google