Conference item icon

Conference item

Initial limit Datalog: a new extensible class of decidable constrained Horn clauses

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 fir...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
0.1109/LICS52264.2021.9470527

Authors


More by this author
Institution:
University of Oxford
Oxford college:
Pembroke College
Role:
Author
More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
ORCID:
0000-0001-7509-680X
More by this author
Institution:
University of Oxford
Oxford college:
Oriel College
Role:
Author
ORCID:
0000-0002-2807-8462
More from this funder
Name:
Engineering & Physical Sciences Research Council
Grant:
EP/M023974/1
Publisher:
IEEE
Host title:
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Publication date:
2021-07-07
Acceptance date:
2021-04-01
Event title:
ACM/IEEE 36th Annual Symposium on Logic in Computer Science (LICS 2021)
Event location:
Online
Event website:
http://easyconferences.eu/lics2021/
Event start date:
2021-06-29
Event end date:
2021-07-02
DOI:
EISBN:
9781665448956
ISBN:
9781665448963
Language:
English
Keywords:
Pubs id:
1170667
Local pid:
pubs:1170667
Deposit date:
2021-04-06

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP