Name
Abstract | ||
|---|---|---|
Clause graph (or connection graph) resolution was invented by Robert Kowalski in 1975. Its behaviour differs significantly from that of traditional resolution in clause sets. Standard notions like completeness do not adequately cover the new phenomena introduced by clause graph resolution and standard proof techniques do not work for clause graphs, which are the major reasons why important questions have been open for years. This paper defines a series of relevant properties in precise terms and answers several of the open questions. The clause graph inference system is refutation complete and refutation confluent. Compared to clause set resolution, clause graph resolution does not increase the complexity of simplest refutations. Many well-known restriction strategies are refutation complete, but most are not refutation confluent for clause graph resolution, which renders them useless. Exhaustive ordering strategies do not exist and contrary to a wide-spread conjecture the plausible approximations of exhaustiveness do not ensure the detection of a refutation. |
Year | DOI | Venue |
|---|---|---|
1986 | 10.1007/3-540-16780-3_100 | CADE |
Keywords | Field | DocType |
strategies,clause graph resolution,completeness,clause graphs,connection graphs,resolution,confluence,graph connectivity,connected graph | Discrete mathematics,Combinatorics,Line graph,Graph property,Computer science,Cubic graph,Directed graph,Null graph,Voltage graph,Graph (abstract data type),Complement graph | Conference |
Volume | ISSN | ISBN |
230 | 0302-9743 | 0-387-16780-3 |
Citations | PageRank | References |
12 | 3.26 | 12 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| N Eisinger | 1 | 12 | 3.26 |