Skip to main content


Constraint modelling: A challenge for first order automated reasoning


Peter Baumgartner and John Slaney



Cadoli et. al. noted the potential of first order automated reasoning for the purpose of analysing constraint models, and reported some encouraging initial experimental results. We are currently pursuing a very similar research program with a view to incorporating deductive technology in a state of the art constraint programming platform. Here we outline our own view of this application direction and discuss new empirical findings on a more extensive range of problems than those considered in the previous literature. While the opportunities presented by reasoning about constraint models are indeed exciting, we also find that there are formidable obstacles in the way of a practicaly useful implementation.

BibTeX Entry

    publisher        = {CEUR Workshop Proceedings},
    author           = {Baumgartner, Peter and Slaney, John},
    issn             = {1613-0073},
    month            = jul,
    editor           = {{Nicolas Peltier and Viorica Sofronie-Stokkermans}},
    year             = {2009},
    title            = {Constraint Modelling: A Challenge for First Order Automated Reasoning},
    booktitle        = {International Workshop on First-Order Theorem Proving (FTP'09)},
    pages            = {4-18},
    address          = {Oslo, Norway}


Served by Apache on Linux on seL4.