Deciding set-theoretic formulae with the predicate 'finite' by a tableau calculus
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.
Downloads
Published
Issue
Section
License
The authors retain all rights to the original work without any restrictions.
License for Published Contents
"Le Matematiche" published articlesa are distribuited with Creative Commons Attribution 4.0 International. You are free to copy, distribute and transmit the work, and to adapt the work. You must attribute the work in the manner specified by the author or licensor (but not in any way that suggests that they endorse you or your use of the work).
License for Metadata
"Le Matematiche" published articles metadata are dedicated to the public domain by waiving all publisher's rights to the work worldwide under copyright law, including all related and neighboring rights, to the extent allowed by law.
You can copy, modify, distribute and perform the work, even for commercial purposes, all without asking permission.
No Fee Charging
No fee is required to complete the submission/review/publishing process of authors paper.
