Constraint Logic Programming over Infinite Domains with an Application to Proof

We present a CLP(FD)-based constraint solver able to deal with unbounded domains. It is based on constraint propagation, resorting to enumeration if all other methods fail. An important aspect is detecting when enumeration was complete and if this has an impact on the soundness of the result. We pre...

Full description

Bibliographic Details
Main Authors: Sebastian Krings, Michael Leuschel
Format: Article
Language:English
Published: Open Publishing Association 2017-01-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1701.00629v1