CARINE とは

CARINEは、一次古典論理自動定理証明者である。
CARINE(Computer Aided Reasoning engine)は深さ優先検索ベースアルゴリズム[Haroun 2005]において、遅延句構造(DCC)と属性シーケンス(ATS)の強化効果の研究のために最初に構築された、 。 CARINEの主な検索アルゴリズムは、繰り返し深化する深度優先探索(深度優先反復深化(DFID)[Korf 1985]としても知られている)に基づいており、THEOのような定理証明者で使用される準線形分解能(SLR) Newborn 2001]。 SLRは、DCCを使用して高い推論速度を達成し、ATSは探索空間を縮小する。