Author: Marc Bezem
Title: Geometric Logic and Proof Objects
Abstract: 
Geometric logic (GL) is the logic preserved by geometric morphisms
between topoi. The first-order fragment of GL extends resolution logic
in that geometric clauses can have existentially quantified
conclusions.  A substantial number of reasoning problems (e.g., in
confluence theory, lattice theory and projective geometry) can be
formulated directly in GL without any skolemization. Thus no skolem
axioms are necessary and the domain of discourse can be kept
finite. These advantages can outweigh the disadvantage that a more
expressive logic is generally more difficult to implement than a
simpler one. We explore the balance between the advantages and
disadvantages with an implementation in Prolog of (incomplete) proof
search in GL including the generation of proof objects. If a proof has
been obtained it can be verified directly in Coq.