The Coq mailing list

[Steve Kremer <kremer AT lsv.ens-cachan.fr>]

                               Séminaire
                 Laboratoire Spécification et Vérification
                        http://www.lsv.ens-cachan.fr/




Mercredi 14 décembre 2005, à 11 h, Salle de conférence (Pavillon des 
Jardins)


Hans de Nivelle (Max-Planck Institut) fera un exposé sur

"Geometric Resolution"

Abstract:

We present a new calculus for first-order logic with equality and 
function symbols. We call the calculus 'geometric resolution' because it 
 operates on geometric formulas.

We introduce geometric formulas and show that every first-order formula 
can be transformed into a geometric formula. An interesting feature of 
the transformation is that it does not depend on Skolemization.

Next we introduce the derivation rules of geometric resolution. We show that
- Geometric resolution is sound.
- It is refutationally complete.
- It is weakly complete for finite models. (This implies that it is 
guaranteed to find models for satisfiable formulas in most of the 
standard decidable classes, like e.g. the 2-variable fragment, or the 
guarded fragment)

We present some results from a preliminary implementation, and discuss 
options how the calculus could be implemented efficiently.

[This is joint work with Jia Meng]

Cordialement,

---
Steve Kremer

Laboratoire Spécification et Vérification
CNRS & INRIA Futurs projet SECSI & École Normale Supérieure de Cachan
61, avenue du Président Wilson
94235 CACHAN Cedex - France
kremer AT lsv.ens-cachan.fr
                http://www.lsv.ens-cachan.fr/~kremer
Tel.: ++ 33 1 47 40 75 45               Secret.: ++ 33 1 47 40 75 20
Fax : ++ 33 1 47 40 75 21               Office : RH-B-102