hide
Free keywords:
-
Abstract:
We present a proof search procedure which is
complete for first-order logic, but which also can be
used when searching for finite models.
The procedure uses a normal form that is closely related to
geometric formulas. For this reason, we call the procedure
geometric resolution.
We expect that the procedure can be used as an efficient
proof search procedure for first-order logic.
We will point out how the procedure can be implemented
in such a way that it is complete for finite models
without loosing completeness for unsatisfiability.
We will also discuss two refinements of the initial procedure,
namely subsumption and functional reduction, and prove
their completeness.
Finally, we will discuss how the calculus can be implemented.