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.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.