Towards Geometrical Models of Proof Systems and Hidden Resolution Proofs

Annelies Gerber


It may be of interest to characterise certain information from logic
geometrically. Any geometrical model of proofs for instance has to be
able to deal with their non-deterministic behaviour. Mathematical
structures such as Boolean algebras can reflect certain properties of
propositional logic. Apart from finding geometries that deal with
non-deterministic behaviour another aim of this research is to find
analogies between existing structures from mathematics or physics and
structures from logic. All mathematical models of proofs need to
reflect the complexity of the corresponding proofs.

We present some first examples of analogies based on Euclidean
geometry for certain input resolution proofs. We also discuss
how unit resolution proofs can be viewed as particular sequences
of completely inelastic particle collisions.

Thursday 6th December 2007, 14:00
Board Room
Department of Computer Science