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.
Herbrand-satisfiability of a Quantified Set-theoretic Fragment
CANTONE, Domenico;LONGO, CRISTIANO;NICOLOSI ASMUNDO, MARIANNA
2017-01-01
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
Herbrand-satisfiability of a Quantified Set-theoretic Fragment.pdf
solo gestori archivio
Tipologia:
Documento in Pre-print
Dimensione
403.37 kB
Formato
Adobe PDF
|
403.37 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.