More Web Proxy on the site http://driver.im/

research-article

Detecting Decidable Classes of Finitely Ground Logic Programs with Function Symbols

Authors:

Marco Calautti,

Irina TrubitsynaAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 18, Issue 4

Article No.: 28, Pages 1 - 42

https://doi.org/10.1145/3143804

Published: 16 November 2017 Publication History

Abstract

In this article, we propose a new technique for checking whether the bottom-up evaluation of logic programs with function symbols terminates. The technique is based on the definition of mappings from arguments to strings of function symbols, representing possible values which could be taken by arguments during the bottom-up evaluation. Starting from mappings, we identify mapping-restricted arguments, a subset of limited arguments, namely arguments that take values from finite domains. Mapping-restricted programs, consisting of rules whose arguments are all mapping restricted, are terminating under the bottom-up computation, as all of its arguments take values from finite domains. We show that mappings can be computed by transforming the original program into a unary logic program: this allows us to establish decidability of checking if a program is mapping restricted. We study the complexity of the presented approach and compare it to other techniques known in the literature. We also introduce an extension of the proposed approach that is able to recognize a wider class of logic programs. The presented technique provides a significant improvement, as it can detect terminating programs not identified by other criteria proposed so far. Furthermore, it can be combined with other techniques to further enlarge the class of programs recognized as terminating under the bottom-up evaluation.

References

[1]

Sabrina Baselice, Piero A. Bonatti, and Giovanni Criscuolo. 2009. On finitely recursive programs. Theory and Practice of Logic Programming 9, 2, 213--238.

Digital Library

[2]

Catriel Beeri and Moshe Y. Vardi. 1984. A proof procedure for data dependencies. Journal of the ACM 31, 4, 718--741.

Digital Library

[3]

Piero A. Bonatti. 2004. Reasoning with infinite stable models. Artificial Intelligence 156, 1, 75--111.

Digital Library

[4]

Maurice Bruynooghe, Michael Codish, John P. Gallagher, Samir Genaim, and Wim Vanhoof. 2007. Termination analysis of logic programs through combination of type-based norms. ACM Transactions on Programming Languages and Systems 29, 2, 10.

Digital Library

[5]

Marco Calautti, Georg Gottlob, and Andreas Pieris. 2015. Chase termination for guarded existential rules. In Proceedings of the 34th ACM Symposium on Principles of Database Systems (PODS’15). 91--103.

Digital Library

[6]

Marco Calautti, Sergio Greco, Cristian Molinaro, and Irina Trubitsyna. 2015a. Logic program termination analysis using atom sizes. In Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI’15). 2833--2839.

Digital Library

[7]

Marco Calautti, Sergio Greco, Cristian Molinaro, and Irina Trubitsyna. 2015b. Rewriting-based check of chase termination. In Proceedings of the 9th Alberto Mendelzon International Workshop on Foundations of Data Management.

[8]

Marco Calautti, Sergio Greco, Cristian Molinaro, and Irina Trubitsyna. 2016a. Using linear constraints for logic program termination analysis. Theory and Practice of Logic Programming 16, 3, 353--377.

[9]

Marco Calautti, Sergio Greco, Cristian Molinaro, and Irina Trubitsyna. 2016b. Exploiting equality generating dependencies in checking chase termination. Proceedings of the VLDB Endowment 9, 5, 396--407.

Digital Library

[10]

Marco Calautti, Sergio Greco, Francesca Spezzano, and Irina Trubitsyna. 2015c. Checking termination of bottom-up evaluation of logic programs with function symbols. Theory and Practice of Logic Programming 15, 6, 854--889.

[11]

Marco Calautti, Sergio Greco, and Irina Trubitsyna. 2013. Detecting decidable classes of finitely ground logic programs with function symbols. In Principles and Practice of Declarative Programming. ACM, New York, NY, 239--250.

Digital Library

[12]

Andrea Calì, Georg Gottlob, and Michael Kifer. 2013. Taming the infinite chase: Query answering under expressive relational constraints. Journal of Artificial Intelligence Research 48, 115--174.

[13]

Francesco Calimeri, Susanna Cozza, Giovambattista Ianni, and Nicola Leone. 2008. Computable functions in ASP: Theory and implementation. In Proceedings of the International Conference on Logic Programming. 407--424.

Digital Library

[14]

Luciano Caroprese, Irina Trubitsyna, and Ester Zumpano. 2007. Implementing prioritized reasoning in logic programming. In Proceedings of the 9th International Conference on Enterprise Information Systems (ICEIS’07), Vol. AIDSS. 94--100.

[15]

Marco A. Casanova, Ronald Fagin, and Christos H. Papadimitriou. 1984. Inclusion dependencies and their interaction with functional dependencies. Journal of Computer and System Sciences 28, 1, 29--59.

[16]

Michael Codish, Vitaly Lagoon, and Peter J. Stuckey. 2005. Testing for termination with monotonicity constraints. In Proceedings of the International Conference on Logic Programming. 326--340.

Digital Library

[17]

Alin Deutsch, Alan Nash, and Jeffrey B. Remmel. 2008. The chase revisited. In Proceedings of the 27th ACM Symposium on Principles of Database Systems (PODS’08). 149--158.

Digital Library

[18]

Alin Deutsch and Val Tannen. 2003. MARS: A system for publishing XML from mixed and redundant storage. In Proceedings of the International Conference on Very Large Data Bases (VLDB’03). 201--212.

Digital Library

[19]

Ronald Fagin, Phokion G. Kolaitis, Renée J. Miller, and Lucian Popa. 2005. Data exchange: Semantics and query answering. Theoretical Computer Science 336, 1, 89--124.

Digital Library

[20]

Filippo Furfaro, Gianluigi Greco, and Sergio Greco. 2004. Minimal founded semantics for disjunctive logic programs and deductive databases. Theory and Practice of Logic Programming 4, 1--2, 75--93.

Digital Library

[21]

Martin Gebser, Torsten Schaub, and Sven Thiele. 2007. GrinGo: A new grounder for answer set programming. In Proceedings of the International Conference on Logic Programming and Nonmonotonic Reasoning. 266--271.

Digital Library

[22]

Allen Van Gelder, Kenneth A. Ross, and John S. Schlipf. 1991. The well-founded semantics for general logic programs. Journal of the ACM 38, 3, 620--650.

Digital Library

[23]

Michael Gelfond and Vladimir Lifschitz. 1988. The stable model semantics for logic programming. In Proceedings of the International Joint Conference and Symposium on Logic Programming. 1070--1080.

[24]

Michael Gelfond and Vladimir Lifschitz. 1991. Classical negation in logic programs and disjunctive databases. New Generation Computing 9, 3--4, 365--386.

[25]

Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. 2014. Proving termination of programs automatically with AProVE. In Proceedings of the 7th International Joint Conference on Automated Reasoning. 184--191.

[26]

T. Gogacz and J. Marcinkowski. 2014. All-instances termination of chase is undecidable. In Proceedings of the International Colloquium on Automata, Languages, and Programming (ICALP’14). 293--304.

[27]

Bernardo Cuenca Grau, Ian Horrocks, Markus Krotzsch, Clemens Kupke, Despoina Magka, Boris Motik, and Zhe Wang. 2013. Acyclicity notions for existential rules and their application to query answering in ontologies. Journal of Artificial Intelligence Research 47, 741--808.

[28]

Sergio Greco, Cristian Molinaro, and Francesca Spezzano. 2012a. Incomplete Data and Data Dependencies in Relational Databases. Morgan 8 Claypool Publishers.

Digital Library

[29]

Sergio Greco, Cristian Molinaro, and Irina Trubitsyna. 2013a. Checking logic program termination under bottom-up evaluation. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI’13).

[30]

Sergio Greco, Cristian Molinaro, and Irina Trubitsyna. 2013b. Logic programming with function symbols: Checking termination of bottom-up evaluation through program adornments. Theory and Practice of Logic Programming 13, 4--5, 737--752.

[31]

Sergio Greco and Francesca Spezzano. 2010. Chase termination: A constraints rewriting approach. Proceedings of the VLDB Endowment 3, 1, 93--104.

Digital Library

[32]

Sergio Greco, Francesca Spezzano, and Irina Trubitsyna. 2011. Stratification criteria and rewriting techniques for checking chase termination. Proc.eedings of the VLDB Endowment 4, 11, 1158--1168.

[33]

Sergio Greco, Francesca Spezzano, and Irina Trubitsyna. 2012b. On the termination of logic programs with function symbols. In Proceedings of the International Conference on Logic Programming (Technical Communications). 323--333.

[34]

Sergio Greco, Francesca Spezzano, and Irina Trubitsyna. 2015. Checking chase termination: Cyclicity analysis and rewriting techniques. IEEE Transactions on Knowledge Data Engineering 27, 3, 621--635.

[35]

Sergio Greco, Irina Trubitsyna, and Ester Zumpano. 2007. On the semantics of logic programs with preferences. Journal of Artificial Intelligence Research 30, 501--523.

Digital Library

[36]

Yuliya Lierler and Vladimir Lifschitz. 2009. One more decidable class of finitely ground programs. In Proceedings of the International Conference on Logic Programming. 489--493.

Digital Library

[37]

Massimo Marchiori. 1996. Proving existential termination of normal logic programs. In Algebraic Methodology and Software Technology. Lecture Notes in Computer Science, Vol. 1101. Springer, 375--390.

Digital Library

[38]

Bruno Marnette. 2009. Generalized schema-mappings: From termination to tractability. In Proceedings of the 28th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS’09). 13--22.

Digital Library

[39]

Arne Meier, Martin Mundhenk, Michael Thomas, and Heribert Vollmer. 2008. The complexity of satisfiability for fragments of CTL and CTL. Electronic Notes on Theoretical Computer Science 223, 201--213.

Digital Library

[40]

Michael Meier, Michael Schmidt, and Georg Lausen. 2009. On chase termination beyond stratification. arXiv:0906.4228.

Digital Library

[41]

Manh Thang Nguyen, Jürgen Giesl, Peter Schneider-Kamp, and Danny De Schreye. 2007. Termination analysis of logic programs based on dependency graphs. In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation. 8--22.

[42]

Manh Thang Nguyen, Danny De Schreye, Jürgen Giesl, and Peter Schneider-Kamp. 2011. Polytool: Polynomial interpretations as a basis for termination analysis of logic programs. Theory and Practice of Logic Programming 11, 1, 33--63.

Digital Library

[43]

Naoki Nishida and Germán Vidal. 2010. Termination of narrowing via termination of rewriting. Applicable Algebra in Engineering, Communication and Computing 21, 3, 177--225.

Digital Library

[44]

Enno Ohlebusch. 2001. Termination of logic programs: Transformational methods revisited. Applicable Algebra in Engineering, Communication and Computing 12, 1--2, 73--116.

[45]

Adrian Onet. 2013. The chase procedure and its applications in data exchange. In Data Exchange, Integration, and Streams, P. G. Kolaitis, M. Lenzerini, and N. Schwiekardt (Eds.). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 1--37.

[46]

Peter Schneider-Kamp, Jürgen Giesl, and Manh Thang Nguyen. 2009a. The dependency triple framework for termination of logic programs. In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation. 37--51.

Digital Library

[47]

Peter Schneider-Kamp, Jürgen Giesl, Alexander Serebrenik, and René Thiemann. 2009b. Automated termination proofs for logic programs by term rewriting. ACM Transactions on Computational Logic 11, 1, Article No. 2.

Digital Library

[48]

Peter Schneider-Kamp, Jürgen Giesl, Thomas Stroder, Alexander Serebrenik, and René Thiemann. 2010. Automated termination analysis for logic programs with cut. Theory and Practice of Logic Programming 10, 4-6, 365--381.

Digital Library

[49]

Danny De Schreye and Stefaan Decorte. 1994. Termination of logic programs: The never-ending story. Journal of Logic Programming 19--20, 1, 199--260.

[50]

Alexander Serebrenik and Danny De Schreye. 2005. On termination of meta-programs. Theory and Practice of Logic Programming 5, 3, 355--390.

Digital Library

[51]

A. Prasad Sistla and Edmund M. Clarke. 1985. The complexity of propositional linear temporal logics. Journal of the ACM 32, 3, 733--749.

Digital Library

[52]

Tran Cao Son, Enrico Pontelli, and Phan Huy Tu. 2007. Answer sets for logic programs with arbitrary abstract constraint atoms. Journal of Artificial Intelligence Research 29, 353--389.

Digital Library

[53]

Tommi Syrjanen. 2001. Omega-restricted logic programs. In Proceedings of the International Conference on Logic Programming and Nonmonotonic Reasoning. 267--279.

Digital Library

[54]

Dean Voets and Danny De Schreye. 2011. Non-termination analysis of logic programs with integer arithmetics. Theory and Practice of Logic Programming 11, 4--5, 521--536.

Cited By

Robaldo LBatsakis SCalegari RCalimeri FFujita MGovernatori GMorelli MPacenza FPisano GSatoh KTachmazidis IZangari J(2024)Compliance checking on first-order knowledge with conflicting and compensatory norms: a comparison among currently available technologiesArtificial Intelligence and Law10.1007/s10506-023-09360-z32:2(505-555)Online publication date: 1-Jun-2024
https://dl.acm.org/doi/10.1007/s10506-023-09360-z
Calautti MCaroprese LGreco SMolinaro CTrubitsyna IZumpano EDesai BCho W(2020)Consistent query answering with prioritized active integrity constraintsProceedings of the 24th Symposium on International Database Engineering & Applications10.1145/3410566.3410592(1-10)Online publication date: 12-Aug-2020
https://dl.acm.org/doi/10.1145/3410566.3410592
Fiorentino NMolinaro CTrubitsyna I(2020)Approximate Query Answering over Incomplete DataComplex Pattern Mining10.1007/978-3-030-36617-9_13(213-227)Online publication date: 15-Jan-2020
https://doi.org/10.1007/978-3-030-36617-9_13
Show More Cited By

Recommendations

Fast Query Answering over Existential Rules

Enhancing Datalog with existential quantification gives rise to Datalog^∃, a powerful knowledge representation language widely used in ontology-based query answering. In this setting, a conjunctive query is evaluated over a Datalog^∃ program consisting of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 18, Issue 4

October 2017

251 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/3143777

Editor:
Orna Kupferman
School of Computer Science and Engineering, Hebrew University, Israel

Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 November 2017

Accepted: 01 September 2017

Revised: 01 June 2017

Received: 01 June 2016

Published in TOCL Volume 18, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
121
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Robaldo LBatsakis SCalegari RCalimeri FFujita MGovernatori GMorelli MPacenza FPisano GSatoh KTachmazidis IZangari J(2024)Compliance checking on first-order knowledge with conflicting and compensatory norms: a comparison among currently available technologiesArtificial Intelligence and Law10.1007/s10506-023-09360-z32:2(505-555)Online publication date: 1-Jun-2024
https://dl.acm.org/doi/10.1007/s10506-023-09360-z
Calautti MCaroprese LGreco SMolinaro CTrubitsyna IZumpano EDesai BCho W(2020)Consistent query answering with prioritized active integrity constraintsProceedings of the 24th Symposium on International Database Engineering & Applications10.1145/3410566.3410592(1-10)Online publication date: 12-Aug-2020
https://dl.acm.org/doi/10.1145/3410566.3410592
Fiorentino NMolinaro CTrubitsyna I(2020)Approximate Query Answering over Incomplete DataComplex Pattern Mining10.1007/978-3-030-36617-9_13(213-227)Online publication date: 15-Jan-2020
https://doi.org/10.1007/978-3-030-36617-9_13
Lifschitz VLifschitz V(2019)Combinatorial SearchAnswer Set Programming10.1007/978-3-030-24658-7_3(29-50)Online publication date: 30-Aug-2019
https://doi.org/10.1007/978-3-030-24658-7_3

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents