Sacre: A Constraint Satisfaction Problem Based Theorem Prover

Thepurpose of this paper is to present a newapproachfor solvingfirst-order predicatelogic problems stated in conjunctive normal form. Wepropose to combineresolution with the Constraint Satisfaction Problem (CSP) paradigm to prove the inconsistency and find a modelof a problem. Theresulting methodbenefits fromresolution and constraint satisfaction techniques and seemsvery efficient whenconfrontedto someproblemsof the CADE-13 competition.

Authors

• Jean-Michel Richer
• Jean-Jacques Chabrier
• LIRSIA
• Université de Bourgogne

Keywords

No keywords are indexed for this paper.