Deciding the \(E^+\)-class by an a posteriori, liftable order (Q1577484)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Deciding the \(E^+\)-class by an a posteriori, liftable order |
scientific article; zbMATH DE number 1501507
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Deciding the \(E^+\)-class by an a posteriori, liftable order |
scientific article; zbMATH DE number 1501507 |
Statements
Deciding the \(E^+\)-class by an a posteriori, liftable order (English)
0 references
26 July 2001
0 references
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.
0 references
theorem-proving
0 references
decidable classes
0 references
\(E^+\)-class
0 references
liftable order
0 references
