Lower bounds for modal logics
Journal of Symbolic Logic 72 (3):941-958 (2007)
| Abstract | We give an exponential lower bound on number of proof-lines in the proof system K of modal logic, i.e., we give an example of K-tautologies ψ1,ψ2,… s.t. every K-proof of ψi must have a number of proof-lines exponential in terms of the size of ψi. The result extends, for the same sequence of K-tautologies, to the systems K4, Gödel—Löb’s logic, S and S4. We also determine some speed-up relations between different systems of modal logic on formulas of modal-depth one. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,705 |
| External links |
  Try with proxy. |
| Through your library | Configure |
Similar books and articlesJan Krajíček (1997). Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic. Journal of Symbolic Logic 62 (2):457-486.
Sara Negri (2005). Proof Analysis in Modal Logic. Journal of Philosophical Logic 34 (5-6):507 - 544.
Frank Wolter (1997). Superintuitionistic Companions of Classical Modal Logics. Studia Logica 58 (2):229-259.
Pavel Pudlák (1997). Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. Journal of Symbolic Logic 62 (3):981-998.
Maria Bonet, Toniann Pitassi & Ran Raz (1997). Lower Bounds for Cutting Planes Proofs with Small Coefficients. Journal of Symbolic Logic 62 (3):708-728.
Samuel R. Buss (1994). On Gödel's Theorems on Lengths of Proofs I: Number of Lines and Speedup for Arithmetics. Journal of Symbolic Logic 59 (3):737-756.
Maarten Marx (2002). Computing with Cylindric Modal Logics and Arrow Logics, Lower Bounds. Studia Logica 72 (2):233-252.
Arnon Avron, Furio Honsell, Marino Miculan & Cristian Paravano (1998). Encoding Modal Logics in Logical Frameworks. Studia Logica 60 (1):161-208.
Marcelo E. Coniglio & Newton M. Peron (2013). Modal Extensions of Sub-Classical Logics for Recovering Classical Logic. Logica Universalis 7 (1):71-86.
Analytics
Monthly downloads |
Added to index2010-08-24Total downloads2 ( #232,628 of 549,198 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
