The GLiDeS Architecture Backtracks

• 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