Automated Proof Construction in Type Theory using Resolution

Bezem, Marc; Hendriks, Dimitri; de Nivelle, Hans

アイテム詳細

登録内容を編集ファイル形式で保存

一時保存へ追加

タグ情報を表示リリース履歴を表示詳細要約

公開

学術論文

Automated Proof Construction in Type Theory using Resolution

MPS-Authors

/persons/resource/persons44298

de Nivelle, Hans
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

There are no locators available

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

フルテキスト (公開)

公開されているフルテキストはありません

付随資料 (公開)

There is no public supplementary material available

引用

Bezem, M., Hendriks, D., & de Nivelle, H. (2002). Automated Proof Construction in Type Theory using Resolution. Journal of Automated Reasoning, 29, 253-275.

引用: https://hdl.handle.net/11858/00-001M-0000-000F-2F21-E

要旨

We provide techniques to integrate resolution logic with equality in type theory. The results may be rendered as follows: {\bf (1)}. A clausification procedure in type theory, equipped with a correctness proof, all encoded using higher-order primitive recursion. {\bf (2)}. A novel representation of clauses in minimal logic such that the $ \lambda $-representation of resolution steps is linear in the size of the premisses. {\bf (3)}. Availability of the power of resolution theorem provers in interactive proof construction systems based on type theory.