Logical Approaches to Computational Barriers

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 |