Projects per year
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 Datalog Z (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.
Original language | English |
---|---|
Title of host publication | Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021) |
Publisher | Institute of Electrical and Electronics Engineers (IEEE) |
Number of pages | 1 |
ISBN (Electronic) | 9781665448956 |
DOIs | |
Publication status | Published - 7 Jul 2021 |
Event | 2021 36th Annual Symposium on Logic in Computer Science - Online Duration: 29 Jun 2021 → 2 Jul 2021 http://easyconferences.eu/lics2021/ |
Publication series
Name | Proceedings - Symposium on Logic in Computer Science |
---|---|
Volume | 2021-June |
ISSN (Print) | 1043-6871 |
Conference
Conference | 2021 36th Annual Symposium on Logic in Computer Science |
---|---|
Abbreviated title | ACM/IEEE LICS 2021 |
Period | 29/06/21 → 2/07/21 |
Internet address |
Bibliographical note
Funding Information:The US Department of Energy Office of Energy Research funded this work at the Pacific Northwest National Laboratory under contract DE-AC06-76RLO 1830.
Publisher Copyright:
© 2021 IEEE.
Structured keywords
- Programming Languages
Fingerprint
Dive into the research topics of 'Initial Limit Datalog: a new extensible class of decidable constrained Horn clauses'. Together they form a unique fingerprint.Projects
- 1 Active