本節では，逐次アルゴリズムのみを示す。 実際には、これを基にモデル共有型並列アルゴリズム、ならびに モデル分散型並列アルゴリズムが用意されているが、 ここでは省略する。 モデル共有型並列アルゴリズムについての詳しい説明は， [KH95]にあるので、興味を持たれた読者は そちらを参照されたい。
以下に nonground 版 MGTP の逐次アルゴリズムを示す． ホーン節のみを扱うので，場合分けによる分岐は考慮されていない．
ここで，MD はモデル拡張の適用によって生成された(後件)アトム を保持するための配列であり，MD[1] から MD[g-1] までがモデル候補を， MD[g] から MD[s] までがモデル拡張候補 (モデル候補に付加されるべき生成アトムの集合)を表す． モデル候補は空集合，モデル拡張候補は正節の後件アトムの集合で初期化され る ( (0)， (1))．
(3) から (6) までがモデル拡張に対応している． 各混合節の前件部 がモデル候補で充足されているか否かを判定し ( (4) と (5) の条件 の前半)，充足可能であれば後件部の包摂テストを行ない ( (5) の条件の 後半)，包摂されなければMDに加える ( (6))．
(5) の条件部中の Cσ is new は， 生成アトム Cσ のどの要素にも包摂されない (σ' Cσ = MD[i]σ' for ∀i(1≦i≦s) なる σ' が存在しない) ことを表す． 包摂テストについては，ここではこの前方包摂テストのみを扱い， Cσ が MD の要素を包摂している (∃i(1≦i≦s)∃σ'Cσσ' = MD[i] )かを調べる後方包摂テ ストは扱わない。(*1)
その後の (7)から (9)がモデル棄却に対応する．各負節の前件部 がモデル候補またはモデル拡張候補で充足されているかを判定し，充足されて いれば証明手続きは終了する．
(*1) : Cσ に包摂される MD[i] を消去しなければならないので、 データの一貫性を保つ必要性が生じ、前方包摂テストより並列化は難しい。 また、破壊代入を許していない KL1 では、消去の際にコピーが必要になる。