A classification of non-liftable orders for resolution

Hans de Nivelle

doi:10.1007/3-540-63104-6_33

A classification of non-liftable orders for resolution

Hans de Nivelle

Centrum voor Wiskunde en Informatica

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

In this paper we study the completeness of resolution when it is restricted by a non-liftable order and by weak subsumption. A non-liftable order is an order that does not satisfy A ≺ B ⇒ AΘ ≺ BΘ. Clause c₁ weakly subsumes c₂ if c₁ Θ ⊆ c₂, and Θ is a renaming substitution. We show that it is natural to distinguish 2 types of non-liftable orders and 3 types of weak subsumption, which correspond naturally to the 2 types of non-liftable orders. Unfortunately all natural combinations are not complete. The problem of the completeness of resolution with non-liftable orders was left open in ([Nivelle96]). We will also give some good news: Every non-liftable order is complete for clauses of length 2, and can be combined with weak subsumption.

Original language	English
Title of host publication	Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings
Editors	William McCune
Publisher	Springer Verlag
Pages	336-350
Number of pages	15
ISBN (Print)	3540631046, 9783540631040
DOIs	https://doi.org/10.1007/3-540-63104-6_33
Publication status	Published - 1997
Externally published	Yes
Event	14th International Conference on Automated Deduction, CADE 1997 - Townsville, Australia Duration: Jul 13 1997 → Jul 17 1997

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1249
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	14th International Conference on Automated Deduction, CADE 1997
Country/Territory	Australia
City	Townsville
Period	7/13/97 → 7/17/97

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/3-540-63104-6_33

Cite this

de Nivelle, H. (1997). A classification of non-liftable orders for resolution. In W. McCune (Ed.), Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings (pp. 336-350). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1249). Springer Verlag. https://doi.org/10.1007/3-540-63104-6_33

A classification of non-liftable orders for resolution. / de Nivelle, Hans.
Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings. ed. / William McCune. Springer Verlag, 1997. p. 336-350 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1249).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

de Nivelle, H 1997, A classification of non-liftable orders for resolution. in W McCune (ed.), Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1249, Springer Verlag, pp. 336-350, 14th International Conference on Automated Deduction, CADE 1997, Townsville, Australia, 7/13/97. https://doi.org/10.1007/3-540-63104-6_33

de Nivelle H. A classification of non-liftable orders for resolution. In McCune W, editor, Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings. Springer Verlag. 1997. p. 336-350. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-63104-6_33

de Nivelle, Hans. / A classification of non-liftable orders for resolution. Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings. editor / William McCune. Springer Verlag, 1997. pp. 336-350 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{cc5667d694664c0ba6cd1f983a8f9bf2,

title = "A classification of non-liftable orders for resolution",

abstract = "In this paper we study the completeness of resolution when it is restricted by a non-liftable order and by weak subsumption. A non-liftable order is an order that does not satisfy A ≺ B ⇒ AΘ ≺ BΘ. Clause c1 weakly subsumes c2 if c1 Θ ⊆ c2, and Θ is a renaming substitution. We show that it is natural to distinguish 2 types of non-liftable orders and 3 types of weak subsumption, which correspond naturally to the 2 types of non-liftable orders. Unfortunately all natural combinations are not complete. The problem of the completeness of resolution with non-liftable orders was left open in ([Nivelle96]). We will also give some good news: Every non-liftable order is complete for clauses of length 2, and can be combined with weak subsumption.",

author = "\{de Nivelle\}, Hans",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1997.; 14th International Conference on Automated Deduction, CADE 1997 ; Conference date: 13-07-1997 Through 17-07-1997",

year = "1997",

doi = "10.1007/3-540-63104-6\_33",

language = "English",

isbn = "3540631046",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "336--350",

editor = "William McCune",

booktitle = "Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings",

address = "Germany",

}

TY - GEN

T1 - A classification of non-liftable orders for resolution

AU - de Nivelle, Hans

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1997.

PY - 1997

Y1 - 1997

N2 - In this paper we study the completeness of resolution when it is restricted by a non-liftable order and by weak subsumption. A non-liftable order is an order that does not satisfy A ≺ B ⇒ AΘ ≺ BΘ. Clause c1 weakly subsumes c2 if c1 Θ ⊆ c2, and Θ is a renaming substitution. We show that it is natural to distinguish 2 types of non-liftable orders and 3 types of weak subsumption, which correspond naturally to the 2 types of non-liftable orders. Unfortunately all natural combinations are not complete. The problem of the completeness of resolution with non-liftable orders was left open in ([Nivelle96]). We will also give some good news: Every non-liftable order is complete for clauses of length 2, and can be combined with weak subsumption.

AB - In this paper we study the completeness of resolution when it is restricted by a non-liftable order and by weak subsumption. A non-liftable order is an order that does not satisfy A ≺ B ⇒ AΘ ≺ BΘ. Clause c1 weakly subsumes c2 if c1 Θ ⊆ c2, and Θ is a renaming substitution. We show that it is natural to distinguish 2 types of non-liftable orders and 3 types of weak subsumption, which correspond naturally to the 2 types of non-liftable orders. Unfortunately all natural combinations are not complete. The problem of the completeness of resolution with non-liftable orders was left open in ([Nivelle96]). We will also give some good news: Every non-liftable order is complete for clauses of length 2, and can be combined with weak subsumption.

UR - http://www.scopus.com/inward/record.url?scp=84957069473&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84957069473&partnerID=8YFLogxK

U2 - 10.1007/3-540-63104-6_33

DO - 10.1007/3-540-63104-6_33

M3 - Conference contribution

AN - SCOPUS:84957069473

SN - 3540631046

SN - 9783540631040

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 336

EP - 350

BT - Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings

A2 - McCune, William

PB - Springer Verlag

T2 - 14th International Conference on Automated Deduction, CADE 1997

Y2 - 13 July 1997 through 17 July 1997

ER -

A classification of non-liftable orders for resolution

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this