The GLiDeS Architecture
Linear deduction using Model Elimination
Maintains an
A-list
of all A-literals in the deduction
All A-list literals FALSE in models of the model clauses
TRUE B-literals reduce