Deciding the \(E^+\)-class by an a posteriori, liftable order (Q1577484)

Resolution decision procedures make it possible to use proof-theoretic techniques in an originally model-theoretic field. One of the classes decidable by resolution is the \(E^+\)-class. This class is defined as the set of clauses in which all literals have the same set of variables, and are weakly covering. The author shows that the \(E^+\)-class can be decided by a liftable order after all, when it is applied a posteriori. Formerly this was posed as an open problem. The author proves termination for the full \(E^+\)-class, with a fully liftable order, and without saturation rules.