English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Formal reasoning about finite sets and cardinality is an important tool formany applications, including software verification, where very often one needsto reason about the size of a given data structure and not only about what itselements are. The Constraint Logic Programming tool {log} provides a decisionprocedure for deciding the satisfiability of formulas involving very generalforms of finite sets, without cardinality. In this paper we adapt and integratea 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. Inturn, the implementation uses Howe and King's Prolog SAT solver and Prolog'sCLP(Q) library, as an integer linear programming solver. The empiricalevaluation of this implementation based on +250 real verification conditionsshows that it can be useful in practice.

Integrating Cardinality Constraints into Constraint Logic Programming with Sets