@techreport{oai:ipsj.ixsq.nii.ac.jp:00030289,
 author = {山田, 俊行 and Middeldorp, Aart and 井田, 哲雄 and Toshiyuki, Yamada and Aart, Middeldorp and Tetsuo, Ida},
 issue = {83(1996-PRO-009)},
 month = {Sep},
 note = {条件付き等式系εに対する条件付き項書換え系(TR)が健全かつ完全であるととは,εのすべてのモデルにおける等価性(=M_ε)とεのもとで等しいことの証明可能性(〓)とが一致することを意味する.本論文では,oriented CTRSの完全性に関するAvenhausとLoria?Saenzの主張を反駁し,絶対不可約性(bsolute irreduciblit)がoriented CTRSの完全性を保証するのに不適切であることを指摘する.この性質に代え,安定性という性質を導入することにより,oriented CTRSが完全であるための新たな十分条件を提示する.Suzukiらにより提案された,階層合流性をもっOriented CTRSが健全かつ完全であることは,本論文の結果により明らかになる., Soundness and completeness of a conditional term rewriting system (CTRS) for a conditional equational system ε means the equivalence of equality in all models (=M_ε) and the provability by equational reasoning (〓). In this paper a claim of Avenhaus and Loria-Saenz about the completeness of oriented CTRSs is refuted. We point out that absolute irreduciblity is an insufficient for ensuring the completeness of oriented CTRSs. As a substitute, we introduce stability and provide a new sufficient condition for completeness of oriented CTRSs. The level-confluent oriented CTRSs proposed by Suzuki et al. turn out to be sound and complete by using the result in this paper.},
 title = {条件付き項書換え系の健全性と完全性},
 year = {1996}
}