| bis 12. Februar 2007: |
| Übernachtungsbuchung durch Koblenz-Touristik |
| bis 26. Februar 2007: |
| elektronische Einsendung von Titel und Abstrakt |
| bis 28. Februar 2007: |
| Rückmeldung |
| 26. März 2007: |
| Ab 13:00: Anmeldung, 14:00: Beginn |
| 27. März 2007: |
| Spätnachmittag: Ende |
|
|
 |
Zusammenfassung: We present a new calculus for first-order logic with equality and function symbols. We call the calculus 'geometric resolution' because it operates on a formula format that is somwehat similar to geometric formulas. The calculus is refutationally complete. We also hope that the calculus will be good at finding finite models.
We introduce the format of geometric formulas and suggest that every first-order formula can be transformed into a set of geometric formulas.
After that, we outline the proof search algorithm. The algorithm operates by a combination of backtracking and learning.
We mention an implementation of geometric resolution, which we call 'geo'. We give a summary of its performance on the last CASC, and explain our future plans with geo.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
