方向付け不能なホーン節に対する書き換え帰納法

等式論理において，帰納法を用いて証明できる等式のことを（等式）帰納的定理と呼ぶ．帰納的定理は等式論理に基づく計算モデルである項書き換えシステムにおける重要な特徴付けの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)ホーン節の条件部の検証に用いる等式集合を指定した新たな書き換え関係を導入する．

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.