Computability in Europe 2006
Logical Approaches to Computational Barriers

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

Speaker: Annelies Gerber
Author(s): Annelies Gerber
Slot: Array, 17:40-18:00, col. 2


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.  

websites: Arnold Beckmann 2006-04-27