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

DOI10.1145/3625230arXiv2105.03005OpenAlexW3162701640WikidataQ130860092 ScholiaQ130860092MaRDI QIDQ6201710FDOQ6201710

Authors: Maximiliano Cristiá, Gianfranco Rossi 

Publication date: 21 February 2024

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

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.

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)

Cites Work

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

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)