Computability in Europe 2006
Logical Approaches to Computational Barriers
|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||
Warning: date(): It is not safe to rely on the system's timezone settings. You are *required* to use the date.timezone setting or the date_default_timezone_set() function. In case you used any of those methods and you are still getting this warning, you most likely misspelled the timezone identifier. We selected the timezone 'UTC' for now, but please set date.timezone to select your timezone. in /srv/www/htdocs-cs/cie06/conf-code.php on line 135