Regular Talk:
Some Mathematical Properties of Input Resolution Refutations with Non-Tautological Resolvents

Abstract

The question of whether or not a given set S of initial propositional clauses
possesses a resolution proof is far from trivial. We aim to geometrically
reproduce all necessary information encoded in propositional resolution proofs.
Here, we give a mathematical characterisation of propositional input resolution
refutations with non-tautological resolvents based on notions from Euclidean
geometry. For a particular class of such proofs we develop a method to check
whether or not a given set S of initial clauses admits such proofs. We comment
on possible generalisations of this approach.