tacticからのプログラム抽出

• Item type: SIG Technical Reports(1)
• 公開日: 1997-03-28
• タイトル: tacticからのプログラム抽出
• タイトル / 言語: en
• タイトル: Program Extraction from Tactics
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 千葉大学総合情報処理センター
• 著者所属: 東京大学大学院理学系研究科
• 著者所属(英): en
• 著者所属(英): Information Processing Center, Chiba Unviersity
• 著者所属(英): en
• 著者所属(英): Graduate School of Science, University of Tokyo
• 著者名: 戸田, 洋三; 萩谷, 昌己
• 著者名(英): Yozo, Toda; Masami, Hagiya
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 定理証明系の証明記述言語であるtacticからのプログラム抽出における問題について議論する．tacticは証明の構成手順を記述するための制御構造を持っており，プログラムの制御構造にあてはめて考えることができる．本稿ではいくつかの事例をとおしてtacticからプログラムを抽出するために次の2点が重要であることを指摘する．・tacticが扱うgoalのパターンを求めること・goalのパターンを論理体系のなかで表現すること
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: We argue about problems on program extraction from tactics; tactics are used in many theorem proving systems to describe how to construct proofs. Each control structure of tactics can be easily mapped to that of programs. Examining a few cases, we claim that the following are important points. ・obtaining goal patterns which tactics accept and generate ・representing goal patterns inside the logical systems
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10485570
• 書誌情報: 情報処理学会研究報告プログラミング（PRO）; 巻 1997, 号 32(1996-PRO-012), p. 9-14, 発行日 1997-03-28
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会