WEKO3
アイテム
方向付け不能なホーン節に対する書き換え帰納法
https://ipsj.ixsq.nii.ac.jp/records/233819
https://ipsj.ixsq.nii.ac.jp/records/233819073763d3-5228-49f3-9f5b-49c37fdf183f
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO1702006.pdf (110.7 kB)
2026年4月22日からダウンロード可能です。
|
Copyright (c) 2024 by the Information Processing Society of Japan
|
|
| 非会員：¥0, IPSJ:学会員：¥0, PRO:会員：¥0, DLIB:会員：¥0 | ||
| Item type | Trans(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2024-04-22 | |||||||||
| タイトル | ||||||||||
| タイトル | 方向付け不能なホーン節に対する書き換え帰納法 | |||||||||
| タイトル | ||||||||||
| 言語 | en | |||||||||
| タイトル | Rewriting Induction for Non-orientable Horn Clauses | |||||||||
| 言語 | ||||||||||
| 言語 | jpn | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | [発表概要, Unrefereed Presentatin Abstract] | |||||||||
| 資源タイプ | ||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||||
| 資源タイプ | journal article | |||||||||
| 著者所属 | ||||||||||
| 新潟大学大学院自然科学研究科 | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Graduate School of Science and Technology, Niigata University | ||||||||||
| 著者名 |
笠鳥, 謙太
× 笠鳥, 謙太
× 青戸, 等人
|
|||||||||
| 著者名(英) |
Kenta, Kasatori
× Kenta, Kasatori
× Takahito, Aoto
|
|||||||||
| 論文抄録 | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | 等式論理において，帰納法を用いて証明できる等式のことを（等式）帰納的定理と呼ぶ．帰納的定理は等式論理に基づく計算モデルである項書き換えシステムにおける重要な特徴付けの1つであり，代数仕様記述や項書き換えシステムに基づくプログラム検証で重要な概念である．等式帰納的定理の証明法として書き換え帰納法(Reddy, 1990)が知られている．また，方向付け不能な等式を扱えるように書き換え帰納法を拡張した体系(Aoto and Toyama, 2016)も知られている．u1=v1, ... , un=vn ⇒ l=rの形をした論理式をホーン節と呼ぶ．証明する対象を等式からホーン節（条件付き等式）に拡張した書き換え帰納法(栗田・青戸, 2018)も知られている．しかし，栗田らの体系はl>rが満たされるようなホーン節しか扱えないという制約がある．そこで，本発表では，方向づけ不能な等式に対する書き換え帰納法(Aoto and Toyama, 2016)とホーン節に対する書き換え帰納法(栗田・青戸, 2018)を組み合わせ，方向付け不能なホーン節に対する書き換え帰納法を提案し，その健全性を証明する．健全性の証明を与えるために，Aoto and Toyama (2016)の証明において，(1)抽象書き換えの一部を重み付き書き換えに変更し，(2)ホーン節の条件部の検証に用いる等式集合を指定した新たな書き換え関係を導入する． | |||||||||
| 論文抄録(英) | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | In equational logic, an equation that can be proved using induction is called an (equational) inductive theorem. Inductive theorem is one of the important characterization of term rewriting systems, which are computational models based on equational logic, and is an important concept in algebraic specification and program verification based on term rewriting systems. Rewriting induction (Reddy, 1990) is known as a method for proving equational inductive theorems. An extension of Reddy's rewriting induction that can handle unorientable equations has been proposed in (Aoto and Toyama, 2016). A formula of the form u1=v1, ... , un=vn ⇒ l=r is called a Horn clause. A rewriting induction method (Kurita and Aoto, 2018) can deal with Horn clauses, but it can not only handle Horn clauses which satisfy l>r. In this presentation, we propose a rewriting induction method for non-orientable Horn clauses extending rewriting method for non-orientable equations (Aoto and Toyama, 2016) and rewriting induction method for Horn clauses (Kurita and Aoto, 2018), and show its soundness. To give our soundness proof, we modify the proof of (Aoto and Toyama, 2016) as follows: (1) we replace a part of abstract reduction with weighted abstract reduction, and (2) we introduce a new rewrite relation which specifies a set of eqations that can be used to verify conditional part of Horn clauses. | |||||||||
| 書誌レコードID | ||||||||||
| 収録物識別子タイプ | NCID | |||||||||
| 収録物識別子 | AA11464814 | |||||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 17, 号 2, p. 2-2, 発行日 2024-04-22 |
|||||||||
| ISSN | ||||||||||
| 収録物識別子タイプ | ISSN | |||||||||
| 収録物識別子 | 1882-7802 | |||||||||
| 出版者 | ||||||||||
| 言語 | ja | |||||||||
| 出版者 | 情報処理学会 | |||||||||
