A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals

DOI10.1145/3625230MaRDI QIDQ6201710OpenAlexWikidataFDO

Authors Maximiliano Cristiá, Gianfranco Rossi

Publication date 21 February 2024

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2105.03005

zbMATH Keywords

constraint logic programmingdecision procedureset theoryinteger intervals\{log\}

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Abstract: In this paper we extend a decision procedure for the Boolean algebra of finite sets with cardinality constraints ($mathcal{L}_{lvertcdotvert}$) to a decision procedure for $mathcal{L}_{lvertcdotvert}$ extended with set terms denoting finite integer intervals ($mathcal{L}_{[,]}$). In $mathcal{L}_{[,]}$ interval limits can be integer linear terms including emph{unbounded variables}. These intervals are a useful extension because they allow to express non-trivial set operators such as the minimum and maximum of a set, still in a quantifier-free logic. Hence, by providing a decision procedure for $mathcal{L}_{[,]}$ it is possible to automatically reason about a new class of quantifier-free formulas. The decision procedure is implemented as part of the $log$ tool. The paper includes a case study based on the elevator algorithm showing that $log$ can automatically discharge all its invariance lemmas some of which involve intervals.

Cites work

• scientific article; zbMATH DE number 2086594 (Why is no real title available?)
• A class of polynomially solvable range constraints for interval analysis without widenings
• A pearl on SAT and SMT solving in Prolog
• A set solver for finite set relation algebra
• An analysis of arithmetic constraints on integer intervals
• An automatically verified prototype of the Tokeneer ID station specification
• Automated proof of Bell-LaPadula security properties
• Automated reasoning with restricted intensional sets
• Deciding Boolean algebra with Presburger arithmetic
• Improving linear constraint propagation by changing constraint representation
• Maintaining knowledge about temporal intervals
• Model checking interval temporal logics with regular expressions
• Reasoning about temporal relations, the tractable subalgebras of Allen's interval algebra
• Reasoning with finite sets and cardinality constraints in SMT
• Solving quantifier-free first-order constraints over finite sets and binary relations
• The B-Book
• Verification, Model Checking, and Abstract Interpretation

Cited in

(1)

• A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers

This page was built for publication: A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6201710)