Name
Abstract | ||
|---|---|---|
We show that the constructive predicate logic with positive (covariant) quantification is hard for doubly exponential universal time, that is, for the class co-2-Nexptime. Our approach is to represent proof-search as computation of an alternating automaton. The memory of the automaton is structured in a way that strictly corresponds to scopes of the binders used in the constructed proof. This provides an application of automata-theoretic techniques in proof theory. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2981544 | ACM Trans. Comput. Log. |
Keywords | Field | DocType |
Intuitionistic logic,positive quantification,complexity,automata | Intuitionistic logic,Discrete mathematics,EXPTIME,Existential quantification,Covariant transformation,Constructive,Automaton,Proof theory,Predicate logic,Mathematics | Journal |
Volume | Issue | ISSN |
17 | 4 | 1529-3785 |
Citations | PageRank | References |
0 | 0.34 | 9 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Aleksy Schubert | 1 | 80 | 17.99 |
| Pawel Urzyczyn | 2 | 333 | 33.29 |
| Daria Walukiewicz-Chrząszcz | 3 | 26 | 3.35 |