Computability in Europe 2006
Logical Approaches to Computational Barriers

Print current page  Print this page

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

Speaker: Annelies Gerber
Author(s): Annelies Gerber
Presentation: GerberCIE06.pdf
Slot: Sat, 17:40-18:00, Faraday C (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 Valid HTML 4.01! Valid CSS! eXTReMe Tracker hit counters by