Computability in Europe 2006
Logical Approaches to Computational Barriers
Logical Approaches to Computational Barriers
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) |
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.
| websites: Arnold Beckmann | 2006-04-27
|