Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Herbrand-satisfiability of a Quantified Set-theoretic Fragment

Cantone D., Longo C., Nicolosi-Asmundo M.

Fundamenta Informaticae

2017

Vol. 150, nr 1

49--71

In the last decades, several fragments of set theory have been studied in the context of Computable Set Theory. In general, the semantics of set-theoretic languages differs from the canonical first-order semantics in that the interpretation domain of set-theoretic terms is fixed to a given universe of sets. Because of this, theoretical results and various machinery developed in the context of first-order logic could be not easily applicable in the set-theoretic realm. Recently, the decidability of quantified fragments of set theory which allow one to explicitly handle ordered pairs has been studied, in view of applications in the field of knowledge representation. Among other results, a NEXPTIME decision procedure for satisfiability of formulae in one of these fragments, ∀0π , has been devised. In this paper we exploit the main features of such a decision procedure to reduce the satisfiability problem for the fragment ∀0π to the problem of Herbrand satisfiability for a first-order language extending it. In addition, it turns out that such a reduction maps formulae of the Disjunctive Datalog subset of ∀0π into Disjunctive Datalog formulae.

On the Satisfiability Problem for a 4-level Quantified Syllogistic and Some Applications to Modal Logic

Cantone D., Asmundo M. N.

Fundamenta Informaticae

2013

Vol. 124, nr 4

427--448

We introduce a multi-sorted stratified syllogistic, called 4LQSR, admitting variables of four sorts and a restricted form of quantification over variables of the first three sorts, and prove that it has a solvable satisfiability problem by showing that it enjoys a small model property. Then, we consider the fragments (4LQSR)h of 4LQSR, consisting of 4LQSR-formulae whose quantifier prefixes have length bounded by h ≥⃒ 2 and satisfying certain additional syntactical constraints, and prove that each of them has an NP-complete satisfiability problem. Finally we show that the modal logic K45 can be expressed in (4LQSR)3.