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

2021/05/06 by Maximiliano Cristiá, Cristiá, Maximiliano, Gianfranco Rossi +1 · 2 citations
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Software Engineering (cs.SE)

paper · pdf · doi:10.48550/arxiv.2105.03005

openalex publication_date 2021/05/06 · openalex created_date 2023/09/24 · openalex updated_date 2026/07/28

Abstract

In this paper we extend a decision procedure for the Boolean algebra of finite sets with cardinality constraints (L_|⋅|) to a decision procedure for L_|⋅| extended with set terms denoting finite integer intervals (L_{[ ]}). In L_{[ ]} interval limits can be integer linear terms including 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 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.

Cited by

• Encoding and Reasoning about Arrays in Constraint Logic Programming with Sets
• From a Constraint Logic Programming Language to a Formal Verification Tool

Related

• A Set-Theoretic Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted Quantifiers
• Integrating Cardinality Constraints into Constraint Logic Programming\n with Sets
• An Effective Decision Procedure for Linear Arithmetic with Integer and Real Variables
• The First-Order Theory of Sets with Cardinality Constraints is Decidable
• Automated Reasoning with Restricted Intensional Sets