Sacre: A Constraint Satisfaction Problem Based Theorem Prover
Abstract
The purpose of this paper is to present a new approach for solving first-order predicate logic 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.
Cite
Text
Richer and Chabrier. "Sacre: A Constraint Satisfaction Problem Based Theorem Prover." AAAI Conference on Artificial Intelligence, 1999.Markdown
[Richer and Chabrier. "Sacre: A Constraint Satisfaction Problem Based Theorem Prover." AAAI Conference on Artificial Intelligence, 1999.](https://mlanthology.org/aaai/1999/richer1999aaai-sacre/)BibTeX
@inproceedings{richer1999aaai-sacre,
title = {{Sacre: A Constraint Satisfaction Problem Based Theorem Prover}},
author = {Richer, Jean-Michel and Chabrier, Jean-Jacques},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {1999},
pages = {306-311},
url = {https://mlanthology.org/aaai/1999/richer1999aaai-sacre/}
}