連言照合における冗長性除去

基本MGTPの連言照合では、前件リテラルとモデル候補M中のアトムの同じ組合せに対して重複した計算が行なわれる可能性がある。このような連言照合における冗長計算を防ぐために RAMS法[FH91]とMERC法が考案されている。

RAMS法

RAMS法は、前件の照合の履歴を記憶する機構を設けることにより、連言照合における重複計算を避けるものである。

MERC法では、MG節がn個のリテラルを含むとき、等価な複数のMG節を補う、という処理が必要になる。

RAMS法では前件リテラルに対するモデル候補との照合結果を記憶するので、照合計算の重複はない。それに対し、MERC法では前件の一部は照合を再計算するという冗長性がある。さらに、MERC法では1本のMG節から等価な節を何本か複製しているので、その冗長性は重複して現れる。

一方、 RAMS法では前件リテラルの照合順序が固定化されていることによって無駄な照合を繰り返す可能性がある。それに対し、MERC法では複製した節が前件リテラルの評価順序を公平に行う、という効果によりこの無駄が省かれる。

メモリ消費に関しては、 RAMS法では照合記憶のため、 MERC法では節の複製のために、いずれも余計にメモリを消費する。

このように、RAMS法とMERC法の優劣は必ずしも明確ではない。どちらが有利かは対象の問題に強く依存している。