Herbrand-satisfiability of a Quantified Set-theoretic Fragment

• Autorzy: Cantone, D. , Longo, C. , Nicolosi-Asmundo, M.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

set theory; Herbrand satisfiability

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 150, nr 1
• Strony: 49--71
• Opis fizyczny: Bibliogr. 19 poz., tab.

Twórcy

autor

Cantone, D.

• Dipartimento di Matematica e Informatica, Università di Catania, Italy,

autor

Longo, C.

• Dipartimento di Matematica e Informatica, Università di Catania, Italy,

autor

Nicolosi-Asmundo, M.

• Dipartimento di Matematica e Informatica, Università di Catania, Italy,

Bibliografia

• [1] Cantone D, Longo C, Nicolosi-Asmundo M. A Decidable Quantified Fragment of Set Theory Involving Ordered Pairs with Applications to Description Logics. In: Bezem M (ed.), CSL 2011, volume 12 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 2011 pp. 129-143. ISBN: 978-3-939897-32-3. doi: 10.4230/LIPIcs.CSL.2011.129.
• [2] Horrocks I, Kutz O, Sattler U. The Even More Irresistible SROIQ. In: Proc. of the 10th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR2006). AAAI Press, 2006 pp. 56-67. URL http://www.cs.man.ac.uk/~horrocks/Publications/download/2006/HoKS06a.pdf.
• [3] Kazakov Y. SRIQ and SROIQ are Harder than SHOIQ. In: Baader F, Lutz C, Motik B (eds.), Proceedings of the 21st International Workshop on Description Logics (DL2008), Dresden, Germany, May 13-16, 2008, volume 353 of CEUR Workshop Proceedings. CEUR-WS.org, 2008 pp. 89-116.
• [4] Moschovakis Y. Notes on Set Theory. Springer, second edition, 2005.
• [5] Cantone D, Ferro A, Omodeo E. Computable set theory, volume 6 of International Series of Monographs on Computer Science. Oxford Science Publications. Clarendon Press, Oxford, UK, 1989. ISBN-10: 0198538073, 13: 9780198538073.
• [6] Cantone D, Omodeo E, Policriti A. Set theory for computing: From decision procedures to declarative programming with sets. Monographs in Computer Science. Springer-Verlag, New York, NY, USA. 2001. doi: 10.1007/978-1-4757-3452-2.
• [7] Schwartz IT, Cantone D, Omodeo EG. Computational logic and set theory: Applying formalized logic to analysis. Springer-Verlag, 2011. Foreword by M. Davis. doi:10.1007/978-0-85729-808-9.
• [8] Fitting M. First-order logic and automated theorem proving (2nd ed.). Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1996. ISBN 0-387-94593-8.
• [9] Herbrand J. Investigations in proof theory: The properties of true propositions. In: van Heijenoort J (ed.), From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Source Books in the History of Sciences, pp. 525-581. Harvard University Press, 1967.
• [10] Hustadt U, Motik B, Sattler U. Reasoning in description logics by a reduction to disjunctive datalog. Journal of Automated Reasoning, 2007; 39 (3): 351-384. doi: 10.1007/s10817-007-9080-3.
• [11] Eiter T. Faber W, Leone N, Pfeifer G, Polleres A. A Logic Programming Approach to Knowledge-state Planning: Semantics and Complexity. ACM Trans. Comput. Logic, 2004; 5 (2): 206-263. doi: 10.1145/976706.976708.
• [12] Eiter T. Gottlob G, Mannila H. Disjunctive Datalog. ACM Trans. Database Syst., 1997; 22 (3): 364—418. doi: 10.1145/261124.261126.
• [13] Alviano M, Faber W, Leone N, Manna M. Disjunctive datalog with existential quantifiers: Semantics, decidability, and complexity issues. TPLP, 2012; 12 (4-5): 701-718. doi: 10.1017/S1471068412000257. URL http://dx.doi.org/10.1017/S1471068412000257.
• [14] Gottlob G, Manna M, Morak M, Pieris A. On the Complexity of Ontological Reasoning under Disjunctive Existential Rules. In: Mathematical Foundations of Computer Science 2012 - 37th International Symposium, MFCS 2012, Bratislava, Slovakia, August 27-31, 2012. Proceedings. 2012 pp. 1-18. doi: 10.1007/978-3-642-32589-2_l.
• [15] Alviano M, Faber W, Leone N, Perri S, Pfeifer G, Terracina G. The Disjunctive Datalog System DLV. In: de Moor O, Gottlob G, Furche T, Sellers AJ (eds.), Datalog Reloaded - First International Workshop, Datalog 2010, Oxford, UK, March 16-19, 2010. Revised Selected Papers, volume 6702 of Lecture Notes in Computer Science. Springer, 2011 pp. 282-301. ISBN: 978-3-642-24205-2.
• [16] Leone N. Pfeifer G, Faber W, Eiter T, Gottlob G, Perri S, Scarcello F. The DLV system for knowledge representation and reasoning. ACM Trans. Comput. Log., 2006; 7 (3): 499-562. doi: 10.1145/1149114.1149117. URL http://doi.acm.org/10.1145/1149114.1149117.
• [17] Nonnengart A, Weidenbach C. Computing Small Clause Normal Forms. In: Robinson JA, Voronkov A (eds.), Handbook of Automated Reasoning, Elsevier and MIT Press, 2001 pp. 335-367. URL http://dblp.uni-trier.de/rec/bib/books/el/RV01/NonnengartW01.
• [18] Cantone D, Longo C. A decidable quantified fragment of set theory with ordered pairs and some undecidable extensions. In: Faella M, Murano A (eds.), Proceedings of Third International Symposium on Games, Automata, Logics and Formal Verification, volume 96 of EPTCS. 2012 pp. 224-237. URL http://dx.doi.org/10.4204/EPTCS.96.17.
• [19] Cantone D, Longo C, Nicolosi Asmundo M. A Decision Procedure for a Two-sorted Extension of Multi-Level Syllogistic with the Cartesian Product and Some Map Constructs. In: Faber W, Leone N (eds.), CILC2010: 25th Italian Conference on Computational Logic. 2010 . doi: 10.1016/j.tcs.2014.03.021.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).

Identyfikatory

DOI

10.3233/FI-2017-1460