Proof complexity of non-classical logics

摘要: Proof complexity is an interdisciplinary area of research utilising techniques from logic, complexity, and combinatorics towards the main aim understanding theorem proving procedures. Traditionally, propositional proofs have been object investigation in proof complexity. Due their richer expressivity numerous applications within computer science, also non-classical logics intensively studied a perspective last decade, number impressive results obtained. In these notes we give introduction to this recent field logics. We cover modal, intuitionistic, non-monotonic Some are surveyed, but addition provide full details exponential lower bound for modal due Hrubes [60] explain several sequent calculi default logic [16,13]. To make text self-contained, include necessary background information on classical systems