Relative NAND-clause growth in Neg refutations

Abstract

Any given propositional discourse can be expressed as a NAND-OR theory – a set of OR-clauses (disjunctions of literals) and NAND-clauses (negated conjunctions e.g. ¬(x∧y)) – making NAND-OR theories similar to traditional normal forms such as CNF and DNF. This thesis will discuss the inference system Neg; a non-explosive, sound and refutationally complete resolution system over NAND-OR theories. Of particular interest will be inconsistent theories which can be refuted in Neg by deriving the empty clause. The main result in this thesis will be a counterexample to the conjecture that the NAND-clauses of inconsistent NAND-OR theories need not grow greater than the size of its OR-clauses in the derivation of the empty clause. Further properties of such inconsistency derivations are explored with the aim of analysing the creation NAND-clauses in Neg.