Hostname: page-component-cd9895bd7-dzt6s Total loading time: 0 Render date: 2024-12-26T13:21:48.508Z Has data issue: false hasContentIssue false
  • English
  • Français

SOME MODEL THEORY OF GUARDED NEGATION

Published online by Cambridge University Press:  21 December 2018

VINCE BÁRÁNY ,
MICHAEL BENEDIKT  and
BALDER TEN CATE
VINCE BÁRÁNY
Affiliation:
DEPARTMENT OF COMPUTER SCIENCE UNIVERSITY OF OXFORD 15 PARKS ROAD OXFORD, OX1 3QD, UKE-mail:[email protected]
MICHAEL BENEDIKT
Affiliation:
DEPARTMENT OF COMPUTER SCIENCE UNIVERSITY OF OXFORD 15 PARKS ROAD OXFORD, OX1 3QD, UKE-mail:[email protected]
BALDER TEN CATE
Affiliation:
DEPARTMENT OF COMPUTER SCIENCE UC SANTA CRUZ 1156 HIGH STREET SANTA CRUZ, CA95064, USAE-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

The Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this article we study the model theory of GNFO formulas. Our results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics.

Keywords

03B70guarded negationinterpolationrewriting
Type
Articles
Information
The Journal of Symbolic Logic , Volume 83 , Issue 4 , December 2018 , pp. 1307 - 1344
Copyright
Copyright © The Association for Symbolic Logic 2018 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Abiteboul, S., Hull, R., and Vianu, V., Foundations of Databases, Addison-Wesley, Boston, 1995.Google Scholar
Andréka, H., van Benthem, J., and Németi, I., Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, vol. 27 (1998), pp. 217–274.CrossRefGoogle Scholar
Baader, F., Calvanese, D., McGuinness, D. L., Nardi, D., and Patel-Schneider, P. F. (eds.), The Description Logic Handbook, Cambridge University Press, New York, 2003.Google Scholar
Baget, J.-F., Mugnier, M.-L., Rudolph, S., and Thomazo, M., Complexity Boundaries for Generalized Guarded Existential Rules, 2011, Research Report LIRMM 11006.Google Scholar
Baget, J.-F., Leclère, M., and Mugnier, M.-L., Walking the decidability line for rules with existential variables, Principles of Knowledge Representation and Reasoning (Lin, F., Sattler, U., and Truszczynski, M., editors), AAAI Press, Menlo Park, CA, 2010, pp. 466–476.Google Scholar
Baget, J.-F., Mugnier, M.-L., Rudolph, S., and Thomazo, M., Walking the complexity lines for generalized guarded existential rules, IJCAI 2011 (Walsh, T., editor), AAAI Press/International Joint Conferences on Artificial Intelligence, Menlo Park, CA, 2011, pp. 712–717.Google Scholar
Bárány, V., Benedikt, M., and ten Cate, B., Rewriting guarded negation queries, Mathematical Foundations of Computer Science 2013 (Chatterjee, K. and Sgall, J., editors), Lecture Notes in Computer Science, vol. 8087, Springer, Berlin, 2013, pp. 98–110.Google Scholar
Bárány, V., ten Cate, B., and Segoufin, L., Guarded negation. Journal of the Association for Computing Machinery, vol. 62 (2015), no. 3, pp. 22:1–22:26.CrossRefGoogle Scholar
Bárány, V., Gottlob, G., and Otto, M., Querying the guarded fragment. Logical Methods in Computer Science, vol. 10 (2014), no. 2.CrossRefGoogle Scholar
Bárány, V., ten Cate, B., and Otto, M., Queries with guarded negation. Procedings of the VLDB Endowment, vol. 5 (2012), no. 11, pp. 1328–1339.CrossRefGoogle Scholar
Bárány, V., ten Cate, B., and Segoufin, L., Guarded negation, Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Part II (Aceto, L., Henzinger, M., and Sgall, J., editors), Lecture Notes in Computer Science, vol. 6756, Springer, Berlin, 2011, pp. 356–367.Google Scholar
Benedikt, M., ten Cate, B., and Vanden Boom, M., Effective interpolation and preservation in guarded logics, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14 (Henzinger, T. A. and Miller, D., editors), Association for Computing Machinery, New York, 2014, pp. 13:1–13:10.Google Scholar
Beth, E. W., On Padoa’s method in the theory of definitions. Indagationes Mathematicae, vol. 15 (1953), pp. 330–339.CrossRefGoogle Scholar
Bienvenu, M., Lutz, C., and Wolter, F., Deciding fo-rewritability in EL, Proceedings of the 2012 International Workshop on Description Logics, DL-2012 (Kazakov, Y., Lembo, D., and Wolter, F., editors), CEUR Workshop Proceedings, vol. 846, CEUR-WS.org, 2012.Google Scholar
Bienvenu, M., ten Cate, B., Lutz, C., and Wolter, F., Ontology-based data access: A study through disjunctive datalog, CSP, and MMSNP, Proceedings of the 32nd Symposium on Principles of Database Systems (Hull, R. and Fan, W., editors), PODS ’13, ACM, New York, 2013, pp. 213–224.CrossRefGoogle Scholar
Calì, A., Gottlob, G., and Kifer, M., Taming the infinite chase: Query answering under expressive relational constraints, Principles of Knowledge Representation and Reasoning, KR 2008 (Brewka, G. and Lang, J., editors), AAAI Press, Menlo Park, CA, 2008, pp. 70–80.Google Scholar
Calì, A., Gottlob, G., and Lukasiewicz, T., A general datalog-based framework for tractable query answering over ontologies, Proceedings of the Twenty-Eigth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2009 (Paredaens, J. and Su, J., editors), Association for Computing Machinery, New York, 2009, pp. 77–86.CrossRefGoogle Scholar
Chandra, A. K. and Merlin, P. M., Optimal implementation of conjunctive queries in relational databases, 9th Association for Computing Machinery Symposium on Theory of Computing (Hopcroft, J. E., Fridman, E. P., and Harrison, M. A., editors), ACM, New York, 1977, pp. 77–90.Google Scholar
Chang, C. C. and Keisler, H. J., Model Theory, North-Holland, Amsterdam, 1990.Google Scholar
Craig, W., Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, this Journal, vol. 22 (1957), no. 3, pp. 269–285.Google Scholar
Ebbinghaus, H.-D. and Flum, J., Finite Model Theory, Springer-Verlag, Berlin, 1999.Google Scholar
Fagin, R., Horn clauses and database dependencies. Journal of the Association for Computing Machinery, vol. 29 (1982), no. 4, pp. 952–985.CrossRefGoogle Scholar
Fagin, R., Kolaitis, P. G., Miller, R. J., and Popa, L., Data exchange: Semantics and query answering. Theoretical Computer Science, vol. 336 (2005), no. 1, pp. 89–124.CrossRefGoogle Scholar
Flum, J., Frick, M., and Grohe, M., Query evaluation via tree-decompositions. Journal of the Association for Computing Machinery, vol. 49 (2002), no. 6, pp. 716–752.CrossRefGoogle Scholar
Gogacz, T. and Marcinkowski, J., The hunt for a red spider: Conjunctive query determinacy is undecidable, Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), IEEE Computer Society, Washington, DC, 2015, pp. 281–292.CrossRefGoogle Scholar
Gogacz, T. and Marcinkowski, J., Red spider meets a rainworm: Conjunctive query finite determinacy is undecidable, Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (Milo, T. and Tan, W.-C., editors), PODS ’16, Association for Computing Machinery, New York, 2016, pp. 121–134.CrossRefGoogle Scholar
Gottlob, G., Leone, N., and Scarcello, F., Robbers, marshals, and guards: Game theoretic and logical characterizations of hypertree width. Journal of Computer and Systems Sciences, vol. 66 (2003), no. 4, pp. 775–808.CrossRefGoogle Scholar
Grädel, E., On the restraining power of guards, this Journal, vol. 64 (1999), no. 4, pp. 1719–1742.Google Scholar
Grädel, E. and Otto, M., The freedoms of (guarded) bisimulation, Johan van Benthem on Logic and Information Dynamics (Baltag, A. and Smets, S., editors), Outstanding Contributions to Logic, vol. 5, Springer, Berlin, 2014, pp. 3–31.Google Scholar
Hoogland, E., Definability and interpolation: Model-theoretic investigations, Ph.D. thesis, University of Amsterdam, 2000.Google Scholar
Hoogland, E., Marx, M., and Otto, M., Beth definability for the guarded fragment, Logic Programming and Automated Reasoning, 6th International Conference, LPAR’99 (Ganzinger, H., McAllester, D. A., and Voronkov, A., editors), Lecture Notes in Computer Science, vol. 1705, Springer, Berlin, 1999, pp. 273–285.CrossRefGoogle Scholar
Lenzerini, M., Data Integration: A theoretical perspective, Proceedings of the Twenty-first ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (Popa, L., Abiteboul, S., and Kolaitis, P. G., editors), PODS ’02, Association for Computing Machinery, New York, 2002, pp. 233–246.CrossRefGoogle Scholar
Lutz, C., Piro, R., and Wolter, F., Description logic TBoxes: Model-theoretic characterizations and rewritability, IJCAI 2011 (Walsh, T., editor), AAAI Press/International Joint Conferences on Artificial Intelligence, Menlo Park, CA, 2011, pp. 983–988.Google Scholar
Lutz, C. and Wolter, F., Foundations for uniform interpolation and forgetting in expressive description logics, IJCAI 2011 (Walsh, T., editor), AAAI Press/International Joint Conferences on Artificial Intelligence, Menlo Park, CA, 2011, pp. 989–995.Google Scholar
Marnette, B., Resolution and datalog rewriting under value invention and equality constraints, preprint, 2011, arXiv:1212.0254v1 [cs.DB].Google Scholar
Marx, M., Queries determined by views: Pack your views, Proceedings of the Twenty-Sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (Libkin, L., editor), Association for Computing Machinery, New York, 2007, pp. 23–30.CrossRefGoogle Scholar
Marx, M. and Venema, Y., Multidimensional Modal Logic, Kluwer, Dordrecht, 1997.CrossRefGoogle Scholar
Nash, A., Segoufin, L., and Vianu, V., Views and queries: Determinacy and rewriting. Association for Computing Machinery Transactions on Database Systems, vol. 35 (2010), no. 3, pp. 21:1–21:41.Google Scholar
Onet, A., The chase procedure and its applications in data exchange, Data Exchange, Integration, and Streams (Kolaitis, P. G., Lenzerini, M., and Schweikardt, N., editors), Schloss Dagstuhl – Leibniz–Zentrum für Informatik, Dagstuhl, 2013, pp. 1–37.Google Scholar
Otto, M., Expressive completeness through logically tractable models. Annals of Pure and Applied Logic, vol. 164 (2013), no. 12, pp. 1418–1453.CrossRefGoogle Scholar
Otto, M., Modal and guarded characterisation theorems over finite transition systems. Annals of Pure and Applied Logic, vol. 130 (2004), pp. 173–205.CrossRefGoogle Scholar
Otto, M., Highly acyclic groups, hypergraph covers and the guarded fragment. Journal of the Association for Computing Machinery, vol. 59 (2012), no. 1, pp. 5:1–5:40.CrossRefGoogle Scholar
Rosen, E., Modal logic over finite structures. Journal of Logic Language and Information, vol. 6 (1997), no. 4, pp. 427–439.CrossRefGoogle Scholar
Rossman, B., Homomorphism preservation theorems. Journal of the Association for Computing Machinery, vol. 55 (2008), no. 3, pp. 15:1–15:53.CrossRefGoogle Scholar
Ten Cate, B., Interpolation for extended modal languages, this Journal, vol. 70 (2005), no. 1, pp. 223–234.Google Scholar
Ten Cate, B., Franconi, E., and Seylan, I., Beth definability in expressive description logics, IJCAI 2011 (Walsh, T., editor), AAAI Press/International Joint Conferences on Artificial Intelligence, Menlo Park, CA, 2011, pp. 1099–1106.Google Scholar
Ten Cate, B. and Segoufin, L., Unary negation, 28th International Symposium on Theoretical Aspects of Computer Science, STACS 2011 (Schwentick, T. and Dürr, C., editors), LIPIcs, vol. 9, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Wadern, 2011, pp. 344–355.Google Scholar
van Benthem, J., Modal Logic and Classical Logic, Bibliopolis, Napoli, 1985.Google Scholar
Yannakakis, M., Algorithms for acyclic database schemes, Proceedings of the Seventh International Conference on Very Large Data Bases - Volume 7, VLDB ’81, VLDB Endowment, 1981, pp. 82–94.Google Scholar