Initial limit Datalog: a new extensible class of decidable constrained Horn clauses
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 Da...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
IEEE
2021
|
| _version_ | 1797072087782785024 |
|---|---|
| author | Cathcart Burn, T Ong, C-H Ramsay, S Wagner, D |
| author_facet | Cathcart Burn, T Ong, C-H Ramsay, S Wagner, D |
| author_sort | Cathcart Burn, T |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T23:02:35Z |
| format | Conference item |
| id | oxford-uuid:62a865a2-e12d-49b4-9894-4b88c0e9939f |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T23:02:35Z |
| publishDate | 2021 |
| publisher | IEEE |
| record_format | dspace |
| spelling | oxford-uuid:62a865a2-e12d-49b4-9894-4b88c0e9939f2022-03-26T18:07:47ZInitial limit Datalog: a new extensible class of decidable constrained Horn clausesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:62a865a2-e12d-49b4-9894-4b88c0e9939fEnglishSymplectic ElementsIEEE2021Cathcart Burn, TOng, C-HRamsay, SWagner, DWe 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. |
| spellingShingle | Cathcart Burn, T Ong, C-H Ramsay, S Wagner, D Initial limit Datalog: a new extensible class of decidable constrained Horn clauses |
| title | Initial limit Datalog: a new extensible class of decidable constrained Horn clauses |
| title_full | Initial limit Datalog: a new extensible class of decidable constrained Horn clauses |
| title_fullStr | Initial limit Datalog: a new extensible class of decidable constrained Horn clauses |
| title_full_unstemmed | Initial limit Datalog: a new extensible class of decidable constrained Horn clauses |
| title_short | Initial limit Datalog: a new extensible class of decidable constrained Horn clauses |
| title_sort | initial limit datalog a new extensible class of decidable constrained horn clauses |
| work_keys_str_mv | AT cathcartburnt initiallimitdataloganewextensibleclassofdecidableconstrainedhornclauses AT ongch initiallimitdataloganewextensibleclassofdecidableconstrainedhornclauses AT ramsays initiallimitdataloganewextensibleclassofdecidableconstrainedhornclauses AT wagnerd initiallimitdataloganewextensibleclassofdecidableconstrainedhornclauses |