Abstract | ||
---|---|---|
There are many ways to define complexity in logic. In finite model theory, it is the complexity of describing properties, whereas in proof complexity it is the complexity of proving properties in a proof system. Here we consider several notions of complexity in logic, the connections among them, and their relationship with computational complexity. In particular, we show how the complexity of logics in the setting of finite model theory is used to obtain results in bounded arithmetic, stating which functions are provably total in certain weak systems of arithmetic. For example, the transitive closure function (testing reachability between two given points in a directed graph) is definable using only NL-concepts (where NL is non-deterministic log-space complexity class), and its totality is provable within NL-reasoning. |
Year | DOI | Venue |
---|---|---|
2008 | 10.1007/978-3-540-69407-6_35 | CiE |
Keywords | Field | DocType |
provably total,bounded arithmetic,transitive closure function,certain weak system,computational complexity,proof system,proof complexity,non-deterministic log-space complexity class,finite model theory,transitive closure,directed graph,functional testing,space complexity | Complexity class,PH,Quantum complexity theory,Discrete mathematics,Average-case complexity,Combinatorics,Structural complexity theory,Computer science,Descriptive complexity theory,Proof complexity,Worst-case complexity | Conference |
Volume | ISSN | Citations |
5028 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 15 | 1 |
Name | Order | Citations | PageRank |
---|---|---|---|
Antonina Kolokolova | 1 | 50 | 10.09 |