Conference item
Geometric decision procedures and the VC dimension of linear arithmetic theories
- Abstract:
-
This paper resolves two open problems on linear integer arithmetic (LIA), also known as Presburger arithmetic. First, we give a triply exponential geometric decision procedure for LIA, i.e., a procedure based on manipulating semilinear sets. This matches the running time of the best quantifier elimination and automata-based procedures. Second, building upon our first result, we give a doubly exponential upper bound on the Vapnik–Chervonenkis (VC) dimension of sets definable in LIA, proving...
Expand abstract
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 911.8KB, Terms of use)
-
- Publisher copy:
- 10.1145/3531130.3533372
Authors
Bibliographic Details
- Publisher:
- Association for Computing Machinery
- Host title:
- LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
- Article number:
- 59
- Publication date:
- 2022-08-04
- Acceptance date:
- 2022-04-14
- Event title:
- 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022)
- Event location:
- Haifa, Israel
- Event website:
- https://lics.siglog.org/lics22/
- Event start date:
- 2022-08-02
- Event end date:
- 2022-08-05
- DOI:
- ISBN:
- 9781450393515
Item Description
- Language:
-
English
- Keywords:
- Pubs id:
-
1264254
- Local pid:
-
pubs:1264254
- Deposit date:
-
2022-06-21
Terms of use
- Copyright holder:
- Chistikov et al.
- Copyright date:
- 2022
- Rights statement:
- © 2022 Copyright held by the owner/author(s). Publication rights licensed to ACM.
- Notes:
- This is the accepted manuscript version of the paper. The final version is available online from the Association for Computing Machinery at: https://doi.org/10.1145/3531130.3533372
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record