We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Integrating Cardinality Constraints into Constraint Logic Programming with Sets

Abstract: Formal reasoning about finite sets and cardinality is an important tool for many applications, including software verification, where very often one needs to reason about the size of a given data structure and not only about what its elements are. The Constraint Logic Programming tool {log} provides a decision procedure for deciding the satisfiability of formulas involving very general forms of finite sets, without cardinality. In this paper we adapt and integrate a decision procedure for a theory of finite sets with cardinality into {log}. The proposed solver is proved to be a decision procedure for its formulas. Besides, the new CLP instance is implemented as part of the {log} tool. In turn, the implementation uses Howe and King's Prolog SAT solver and Prolog's CLP(Q) library, as an integer linear programming solver. The empirical evaluation of this implementation based on +250 real verification conditions shows that it can be useful in practice.
Comments: Under consideration in Theory and Practice of Logic Programming (TPLP)
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:2102.05422 [cs.LO]
  (or arXiv:2102.05422v2 [cs.LO] for this version)

Submission history

From: Maximiliano Cristia [view email]
[v1] Wed, 10 Feb 2021 13:38:49 GMT (54kb)
[v2] Tue, 5 Oct 2021 14:53:16 GMT (58kb)

Link back to: arXiv, form interface, contact.