In this paper we present a solver for a first-order logic language where sets and binary relations can be freely and naturally combined. The language can express, at least, any full set relation algebra on finite sets. It provides untyped, hereditarily finite sets, whose elements can be variables, and basically all the classic set and relational operators used in formal languages such as B and Z. Sets are first-class entities in the language, thus they are not encoded in lower level theories. Relations are just sets of ordered pairs. The solver exploits set unification and set constraint solving as primitive features. The solver is proved to be a sound semi-decision procedure for the accepted language. A Prolog implementation is presented and an extensive empirical evaluation provides evidence of its usefulness.

Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations / Cristia, M.; Rossi, G.. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - (2019). [10.1007/s10817-019-09520-4]

Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations

Rossi G.
2019-01-01

Abstract

In this paper we present a solver for a first-order logic language where sets and binary relations can be freely and naturally combined. The language can express, at least, any full set relation algebra on finite sets. It provides untyped, hereditarily finite sets, whose elements can be variables, and basically all the classic set and relational operators used in formal languages such as B and Z. Sets are first-class entities in the language, thus they are not encoded in lower level theories. Relations are just sets of ordered pairs. The solver exploits set unification and set constraint solving as primitive features. The solver is proved to be a sound semi-decision procedure for the accepted language. A Prolog implementation is presented and an extensive empirical evaluation provides evidence of its usefulness.
2019
Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations / Cristia, M.; Rossi, G.. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - (2019). [10.1007/s10817-019-09520-4]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11381/2862510
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 17
  • ???jsp.display-item.citation.isi??? 12
social impact