Deciding the \(E^+\)-class by an a posteriori, liftable order
type: Item
instance of: scholarly article
title: Deciding the \(E^+\)-class by an a posteriori, liftable order
zbMATH Open document ID: 0966.03012
DOI: 10.1016/S0168-0072(00)00013-0
author: Hans de Nivelle
published in: Annals of Pure and Applied Logic
publication date: 2001-07-26T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1501507
zbMATH Keywords: theorem-proving
zbMATH Keywords: decidable classes
zbMATH Keywords: \(E^+\)-class
zbMATH Keywords: liftable order
reviewed by: Nail Zamov
describes a project that uses: OTTER
describes a project that uses: SPASS
describes a project that uses: FLOTTER
MaRDI profile type: Publication
cites work: Q5679729
cites work: Q3905252
cites work: Resolution methods for the decision problem
cites work: Resolution Strategies as Decision Procedures
cites work: Q4331764
cites work: Q3728875
cites work: Q4474846
cites work: Q4249898
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q3348885
cites work: On a bound for the complexity of terms in the resolution method
full work available at URL: s0168-0072(00)00013-0
OpenAlex ID: W2010309877
Wikidata QID: Q127592956
description: scientific article; zbMATH DE number 1501507