WEKO3
アイテム
定理証明手続きとしての高階単一化
https://ipsj.ixsq.nii.ac.jp/records/30867
https://ipsj.ixsq.nii.ac.jp/records/30867504b052e-4b5e-4f39-9e32-08417dfffd41
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-PRO90036003.pdf (1.6 MB)
|
Copyright (c) 1990 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 1990-09-21 | |||||||
| タイトル | ||||||||
| タイトル | 定理証明手続きとしての高階単一化 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Higher - order Unification as a Theorem Proving Procedure | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
| 資源タイプ | technical report | |||||||
| 著者所属 | ||||||||
| 京都大学数理解析研究所 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| RIMS, Kyoto University | ||||||||
| 著者名 |
萩谷, 昌己
× 萩谷, 昌己
|
|||||||
| 著者名(英) |
Masami, Hagiya
× Masami, Hagiya
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | Logical Frameworkなどの高階の型理論における高階の単一化手続きは、軟々対にも射影を許すことにより、定理証明手続きとして用いることができることを指摘する。特に、Logical Frameworkにおける高階の単一化手続きから、プログラム変換によってPrologのインタープリタが得られることを示す。 | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | It is shown that higher-order unification procedures for higher-order type systems such as Logical Framework can be used as a theorem proving procedure if projection is also allowed on flexible-flexible pairs. In particular, Prolog interpreter is derived from a higher-order unification procedure for Logical Framework by program transformation. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN10485570 | |||||||
| 書誌情報 |
情報処理学会研究報告プログラミング（PRO） 巻 1990, 号 76(1990-PRO-036), p. 1-10, 発行日 1990-09-21 |
|||||||
| Notice | ||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
