Sacre: A Constraint Satisfaction Problem Based Theorem Prover

Jean-Michel Richer and Jean-Jacques Chabrier, LIRSIA, Université de Bourgogne

The purpose of this paper is to present a new approach for solving first-order predicate calculus problems stated in conjunctive normal form. We propose to combine resolution with the Constraint Satisfaction Problem (CSP) paradigm to prove the inconsistency and find a model of a problem. The resulting method benefits from resolution and constraint satisfaction techniques and seems very efficient when confronted to some problems of the CADE-13 competition.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.