Conference item icon

Conference item

On the existential theories of Büchi arithmetic and linear p-adic fields

Abstract:

We consider the complexity of the satisfiability problems for the existential fragment of Büchi arithmetic and for the existential fragment of linear arithmetic over p-adic fields. Our main results are that both problems are NP-complete. The NP upper bound for existential linear arithmetic over p-adic fields resolves an open question posed by Weispfenning [J. Symb. Comput., 5(1/2) (1988)] and holds despite the fact that satisfying assignments in both theories may have bit-size super-polynomia...

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

Actions


Access Document


Files:
  • (Accepted manuscript, pdf, 337.7KB)
Publisher copy:
10.1109/LICS.2019.87856810

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
More by this author
Institution:
University of Oxford
Division:
MPLS Division
Department:
Computer Science
Role:
Author
Publisher:
IEEE Publisher's website
Host title:
2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Journal:
ACM/IEEE Symposium on Logic in Computer Science Journal website
Publication date:
2019-08-05
Acceptance date:
2019-03-28
DOI:
ISBN:
9781728136080
Pubs id:
pubs:1003014
UUID:
uuid:a85cdf1b-189c-43b2-8800-105f3b36cfb5
Local pid:
pubs:1003014
Source identifiers:
1003014
Deposit date:
2019-05-24

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