Cited By
View all- Jochems JJones ERamsay S(2023)Higher-Order MSL Horn ConstraintsProceedings of the ACM on Programming Languages10.1145/35712627:POPL(2017-2047)Online publication date: 9-Jan-2023
Initial limit datalog: a new extensible class of decidable constrained horn clauses
Article No.: 46, Pages 1 - 13
Abstract
We present initial limit Datalog, a new extensible class of constrained Horn clauses for which the satisfiability problem is decidable. The class may be viewed as a generalisation to higher-order logic (with a simple restriction on types) of the first-order language limit DatalogZ (a fragment of Datalog modulo linear integer arithmetic), but can be instantiated with any suitable background theory. For example, the fragment is decidable over any countable well-quasi-order with a decidable first-order theory, such as natural number vectors under componentwise linear arithmetic, and words of a bounded, context-free language ordered by the subword relation. Formulas of initial limit Datalog have the property that, under some assumptions on the background theory, their satisfiability can be witnessed by a new kind of term model which we call entwined structures. Whilst the set of all models is typically uncountable, the set of all entwined structures is recursively enumerable, and model checking is decidable.
References
[1]
J. Jaffar and M. J. Maher, "Constraint logic programming: a survey," The Journal of Logic Programming, vol. 19--20, pp. 503--581, 1994, special Issue: Ten Years of Logic Programming.
[2]
N. Bjørner, A. Gurfinkel, K. L. McMillan, and A. Rybalchenko, "Horn clause solvers for program verification," in Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, 2015, pp. 24--51.
[3]
T. Cathcart Burn, C.-H. L. Ong, and S. J. Ramsay, "Higher-order constrained horn clauses for verification," Proc. ACM Program. Lang., vol. 2, no. POPL, pp. 11:1--11:28, Dec. 2017. [Online].
[4]
J. Cox, K. McAloon, and C. Tretkoff, "Computational complexity and constraint logic programming languages," Ann. Math. Artif. Intell., vol. 5, no. 2--4, pp. 163--189, 1992. [Online].
[5]
P. J. Downey, "Undecidability of presburger arithmetic with a single monadic predicate letter," Center for Research in Computer Technology, Harvard University, Technical Report TR-18-72, 1972.
[6]
M. Kaminski, B. Cuenca Grau, E. V. Kostylev, B. Motik, and I. Horrocks, "Foundations of declarative data analysis using limit datalog programs," in Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19--25, 2017, 2017, pp. 1123--1130. [Online].
[7]
C.-H. L. Ong and D. Wagner, "HoCHC: A refutationally complete and semantically invariant system of higher-order logic modulo theories," in 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24--27, 2019, 2019, pp. 1--14. [Online].
[8]
D. Kuske and G. Zetzsche, "Languages ordered by the subword order," in Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6--11, 2019, Proceedings, ser. Lecture Notes in Computer Science, M. Bojanczyk and A. Simpson, Eds., vol. 11425. Springer, 2019, pp. 348--364. [Online].
[9]
A. Finkel and P. Schnoebelen, "Well-structured transition systems everywhere!" Theor. Comput. Sci., vol. 256, no. 1--2, pp. 63--92, 2001. [Online].
[10]
A. Charalambidis, K. Handjopoulos, P. Rondogiannis, and W. W. Wadge, "Extensional higher-order logic programming," ACM Trans. Comput. Log., vol. 14, no. 3, pp. 21:1--21:40, 2013.
[11]
L. Henkin, "Completeness in the theory of types," J. Symb. Log., vol. 15, no. 2, pp. 81--91, 1950.
[12]
J. A. Robinson, "A machine-oriented logic based on the resolution principle," J. ACM, vol. 12, no. 1, pp. 23--41, 1965.
[13]
L. Bachmair, H. Ganzinger, and U. Waldmann, "Refutational theorem proving for hierarchic first-order theories," Appl. Algebra Eng. Commun. Comput., vol. 5, pp. 193--212, 1994.
[14]
S. Schmitz and P. Schnoebelen, "Algorithmic aspects of WQO theories," Tech. Rep., 2017, cMI Lecture Notes. [Online]. Available: http://www.lsv.fr/~phs/algorithmic_aspects_of_wqos.pdf
[15]
S. Halfon, P. Schnoebelen, and G. Zetzsche, "Decidability, complexity, and expressiveness of first-order logic over the subword ordering," in 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20--23, 2017. IEEE Computer Society, 2017, pp. 1--12. [Online].
[16]
P. Alvaro, T. Condie, N. Conway, K. Elmeleegy, J. M. Hellerstein, and R. Sears, "Boom analytics: Exploring data-centric, declarative programming for the cloud," in Proceedings of the 5th European Conference on Computer Systems, ser. EuroSys '10. New York, NY, USA: Association for Computing Machinery, 2010, p. 223--236. [Online].
[17]
T. Cathcart Burn, L. Ong, S. Ramsay, and D. Wagner, "Initial limit datalog: a new extensible class of decidable constrained horn clauses," CoRR, vol. abs/2104.14175, 2021. [Online]. Available: http://arxiv.org/abs/2104.14175
[18]
Y. Manin, A Course in Mathematical Logic for Mathematicians, 01 2010, vol. 53.
[19]
A. Charalambidis, C. Nomikos, and P. Rondogiannis, "The expressive power of higher-order datalog," TPLP, vol. 19, no. 5--6, pp. 925--940, 2019. [Online].
[20]
R. Mayr, "Undecidable problems in unreliable computations," Theoretical Computer Science, vol. 297, no. 1, pp. 337--354, 2003, latin American Theoretical Informatics.
[21]
A. Bouajjani and R. Mayr, "Model checking lossy vector addition systems," in STACS 99, C. Meinel and S. Tison, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999, pp. 323--333.
[22]
A. W. Lin, "Model checking infinite-state systems: Generic and specific approaches," Ph.D. dissertation, University of Edinburgh, 2010.
[23]
V. Barany, "Automatic presentations of infinite structures," Ph.D. dissertation, RWTH Aachen University, 2007.
[24]
B. R. Hodgson, "On direct products of automaton decidable theories," Theor. Comput. Sci., vol. 19, pp. 331--335, 1982. [Online].
[25]
B. Khoussainov and A. Nerode, "Automatic presentations of structures," in Logical and Computational Complexity. Selected Papers. Logic and Computational Complexity, International Workshop LCC '94, Indianapolis, Indiana, USA, 13--16 October 1994, ser. Lecture Notes in Computer Science, D. Leivant, Ed., vol. 960. Springer, 1994, pp. 367--392. [Online].
[26]
E. Dantsin, T. Eiter, G. Gottlob, and A. Voronkov, "Complexity and expressive power of logic programming," ACM Comput. Surv., vol. 33, no. 3, pp. 374--425, 2001.
[27]
Y. Gurevich, "Monadic second-order theories," in Model-Theoretical Logics, J. Barwise and S. Feferman, Eds. Springer-Verlag, 1985, ch. XIII, pp. 479--506.
[28]
M. O. Rabin, "Decidability of second-order theories and automata on infinite trees," Transactions of the American Mathematical Society, vol. 141, pp. 1--35, 1969.
[29]
P. Madhusudan, U. Mathur, S. Saha, and M. Viswanathan, "A decidable fragment of second order logic with applications to synthesis," in Proceedings of CSL'18, 2018, pp. 31:1--31:19.
[30]
N. Kobayashi, T. Tsukada, and K. Watanabe, "Higher-order program verification via HFL model checking," in Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14--20, 2018, Proceedings, 2018, pp. 711--738. [Online].
Index Terms
- Initial limit datalog: a new extensible class of decidable constrained horn clauses
Index terms have been assigned to the content through auto-classification.
Recommendations
Datalog LITE: a deductive query language with linear time model checking
We present Datalog LITE, a new deductive query language with a linear-time model-checking algorithm, that is, linear time data complexity and program complexity. Datalog LITE is a variant of Datalog that uses stratified negation, restricted variable ...
Limit Datalog: A Declarative Query Language for Data Analysis
Motivated by applications in declarative data analysis, we study DatalogZ-an extension of Datalog with stratified negation and arithmetics over integers. Reasoning in this language is undecidable, so we present a fragment, called limit DatalogZ, that is ...
Disjunctive datalog
We consider disjunctive Datalog, a powerful database query language based on disjunctive logic programming. Briefly, disjunctive Datalog is a variant of Datalog where disjunctions may appear in the rule heads; advanced versions also allow for negation in ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sponsors
In-Cooperation
- EACSL: European Association for Computer Science Logic
- IEEE-CS: Computer Society
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 24 November 2021
Check for updates
Qualifiers
- Research-article
Conference
LICS '21
Sponsor:
LICS '21: 36th Annual ACM/IEEE Symposium on Logic in Computer Science
June 29 - July 2, 2021
Rome, Italy
Acceptance Rates
Overall Acceptance Rate 215 of 622 submissions, 35%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 19Total Downloads
- Downloads (Last 12 months)5
- Downloads (Last 6 weeks)2
Reflects downloads up to 01 Mar 2025
Other Metrics
Citations
Cited By
View all- Jochems JJones ERamsay S(2023)Higher-Order MSL Horn ConstraintsProceedings of the ACM on Programming Languages10.1145/35712627:POPL(2017-2047)Online publication date: 9-Jan-2023
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in