test FOO test
Computability in Europe 2006
Logical Approaches to Computational Barriers
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