Deciding set-theoretic formulae with the predicate 'finite' by a tableau calculus

  • Domenico Cantone
  • Rosa Ruggeri Cannata

Abstract

In this paper we give a decidable tableau calculus for the unquantified theory MLSSF, which involves in addition the constructs of Multilevel Syllogistic, namely 'membership', 'equality', 'set inclusion', 'binary union', 'binary intersection' and 'set difference', also finite numerations '., ..., .' and the predicate Finite.

The notions of U-hierarchy and U-realization of a graph w.r.t. given U-sets, as well as some of their properties, are discussed and used to show the soundness and the completeness of the tableau calculus presented.

Published
1995-12-01
Section
Articoli