Incompleteness of the Inference System BNeg

Abstract

Any propositional discourse can be represented as a propositional theory in a specific form in such a way that the theory is inconsistent if and only if the discourse is paradoxical. Propositional theories in this form can be represented as directed graphs such that the models of the theory correspond to the kernels of the digraph. This thesis looks at Neg; a sound, refutationally complete, non-explosive resolution system over such propositional theories. We investigate the relation between various graph structures and clauses provable by the resolution system from the corresponding theory. The main results is a counter-example to a conjecture that a restricted version BNeg of the system is refutationally complete.