Wyniki wyszukiwania - BazTech

Ograniczanie wyników

3 Fundamenta Informaticae

Znaleziono wyników: 3

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: computable set theory

Sortuj według:

Ogranicz wyniki do:

Complexity Assessments for Decidable Fragments of Set Theory. I : A Taxonomy for the Boolean Case

Cantone Domenico, De Domenico Andrea, Maugeri Pietro, Omodeo Eugenio G.

Fundamenta Informaticae

2021

Vol. 181, nr 1

37--69

We report on an investigation aimed at identifying small fragments of set theory (typically, sublanguages of Multi-Level Syllogistic) endowed with polynomial-time satisfiability decision tests, potentially useful for automated proof verification. Leaving out of consideration the membership relator ∈ for the time being, in this paper we provide a complete taxonomy of the polynomial and the NP-complete fragments involving, besides variables intended to range over the von Neumann set-universe, the Boolean operators ∪, ∩, \, the Boolean relators ⊆, ⊈,=, ≠, and the predicates ‘• = Ø’ and ‘Disj(•, •)’, meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘• ≠ Ø and ‘¬Disj(•, •)’. We also examine in detail how to test for satisfiability the formulae of six sample fragments: three sample problems are shown to be NP-complete, two to admit quadratic-time decision algorithms, and one to be solvable in linear time.

An Improved Set-based Reasoner for the Description Logic 𝒟ℒD4,×

Cantone Domenico, Nicolosi-Asmundo Marianna, Santamaria Daniele Francesco

Fundamenta Informaticae

2021

Vol. 178, nr 4

315--346

We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic 𝒟ℒ〈4LQSR,×〉(D ) (𝒟 ℒD 4,×, for short). Our application solves the main TBox and ABox reasoning problems for 𝒟 ℒ D 4,×. In particular, it solves the consistency and the classification problems for 𝒟 ℒD 4,× -knowledge bases represented in set-theoretic terms, and a generalization of the Conjunctive Query Answering problem in which conjunctive queries with variables of three sorts are admitted. The reasoner, which extends and improves a previous version, is implemented in C++. It supports 𝒟 ℒ D 4,×-knowledge bases serialized in the OWL/XML format and it admits also rules expressed in SWRL (Semantic Web Rule Language).

Mapping Sets and Hypersets into Numbers

D’Agostino G., Omodeo E. G., Policriti A., Tomescu A. I.

Fundamenta Informaticae

2015

Vol. 140, nr 3/4

307--328

We introduce and prove the basic properties of encodings that generalize to non-wellfounded hereditarily finite sets the bijection defined by Ackermann in 1937 between hereditarily finite sets and natural numbers.