Sciweavers

CADE
2006
Springer

Geometric Resolution: A Proof Procedure Based on Finite Model Search

15 years 24 days ago
Geometric Resolution: A Proof Procedure Based on Finite Model Search
We present a proof procedure that is complete for first-order logic, but which can also be used when searching for finite models. The procedure uses a normal form which is based on 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 firstorder logic. In addition, the procedure can be implemented in such a way that it is complete for finding finite models.
Hans de Nivelle, Jia Meng
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where CADE
Authors Hans de Nivelle, Jia Meng
Comments (0)