Automated Reasoning with Restricted Intensional Sets

TL;DR

This paper introduces a decision procedure for a first-order logic language with restricted intensional sets, enabling automated reasoning on complex formulas involving such sets, with practical implementation and empirical evaluation.

Contribution

It presents a novel decision procedure for a logic language with restricted intensional sets, including implementation and case studies demonstrating practical applicability.

Findings

The tool can encode and solve many interesting problems with RIS.

Empirical evaluation shows the tool's practical usability.

RIS are sufficiently expressive despite being a subclass of general intensional sets.

Abstract

Intensional sets, i.e., sets given by a property rather than by enumerating elements, are widely recognized as a key feature to describe complex problems (see, e.g., specification languages such as B and Z). Notwithstanding, very few tools exist supporting high-level automated reasoning on general formulas involving intensional sets. In this paper we present a decision procedure for a first-order logic language offering both extensional and (a restricted form of) intensional sets (RIS). RIS are introduced as first-class citizens of the language and set-theoretical operators on RIS are dealt with as constraints. Syntactic restrictions on RIS guarantee that the denoted sets are finite, though unbounded. The language of RIS, called L_RIS , is parametric with respect to any first-order theory X providing at least equality and a decision procedure for X-formulas. In particular, we consider the instance of L_RIS when X is the theory of hereditarily finite sets and binary relations. We also present a working implementation of this instance as part of the {log} tool and we show through a number of examples and two case studies that, although RIS are a subclass of general intensional sets, they are still sufficiently expressive as to encode and solve many interesting problems. Finally, an extensive empirical evaluation provides evidence that the tool can be used in practice.