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...
Hauptverfasser: | Cathcart Burn, T, Ong, C-H, Ramsay, S, Wagner, D |
---|---|
Format: | Conference item |
Sprache: | English |
Veröffentlicht: |
IEEE
2021
|
Ähnliche Einträge
-
Higher-order constrained horn clauses for verification
von: Cathcart Burn, T, et al.
Veröffentlicht: (2017) -
Datalog rewritability of Disjunctive Datalog programs and non-Horn ontologies
von: Cuenca Grau, B, et al.
Veröffentlicht: (2016) -
Computing Datalog Rewritings Beyond Horn Ontologies
von: Grau, B, et al.
Veröffentlicht: (2013) -
Datalog rewriting techniques for non-Horn ontologies
von: Kaminski, M, et al.
Veröffentlicht: (2014) -
Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions
von: Qi Zhou, et al.
Veröffentlicht: (2018-09-01)