Publisher's Synopsis
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 and problems 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 thesis aims to define a series of relevant properties in precise terms and answer several of the open questions. The clause graph inference system is refutation complete and refutation confluent if the insertion of a single additional variant of a clause into the graph is allowed. Compared to clause set resolution, clause graph resolution does not increase the complexity of simplest refutations, again provided that one additional variant may be inserted.;A number of 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.
