講演抄録/キーワード |
講演名 |
2008-07-31 17:30
制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序 ○西田直樹・坂田 翼・酒井正彦・草刈圭一朗・坂部俊樹(名大) SS2008-20 |
抄録 |
(和) |
定理自動証明では手続きが停止せずに暴走してしまうことがある.その暴走
を避けるために,制約付き項書換えに対する定理自動証明の手続きが潜在帰
納法と書換え帰納法それぞれに対して提案された.一方,書換えが停止性を
持つにもかかわらず,計算が進むにつれて項に含まれる書換え可能な項の大
きさが増大していく場合がある.このような書換え系での定理自動証明にお
いて,書換え系の停止性を保存するように等式を方向付けして追加すること
は,経路順序を用いる手法では困難である.本稿では,引数切り落とし法を
導入しながら,制約付き書換え系の停止性を保存する等式の方向付けに適し
た簡約化順序の条件を示す.制約付きTRSの潜在帰納法と書換え帰納法におけ
る定理証明での等式の方向付けにおいて,その条件を満たす簡約化順序が有
効であることを示す. |
(英) |
In automated theorem proving, we often face cases where the procedure
keeps running. To avoid such cases, the theorem proving methods based
on implicit and rewriting inductions have been proposed for constrained
rewriting systems. On the other hand, in terminating term rewriting,
there are some cases where computation is reducing while the size of
reducible terms is increasing. In (automated) theorem proving for
rewriting systems with such cases, it is very difficult
(or near-impossible) to orient equations by path-based reduction orders
in order to add the equations into the rewriting systems, preserving
termination of the rewriting systems. In this paper, introducing the
argument filtering technique, we show a condition of reduction orders
that can be used in orienting equations with preserving termination of
constrained systems. We also show that reduction orders satisfying the
condition are effective for orientation phases in theorem proving methods
based on implicit induction or rewriting induction for constrained term
rewriting systems. |
キーワード |
(和) |
停止性 / 簡約化対 / 引数切り落とし法 / 潜在帰納法 / 書換え帰納法 / / / |
(英) |
termination / reduction pair / argument filtering / implicit induction / rewriting induction / / / |
文献情報 |
信学技報, vol. 108, no. 173, SS2008-20, pp. 43-48, 2008年7月. |
資料番号 |
SS2008-20 |
発行日 |
2008-07-24 (SS) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
SS2008-20 |