Citations of:
Frege systems for extensible modal logics
Annals of Pure and Applied Logic 142 (1):366379 (2006)
Add citations
You must login to add citations.




We show that IPC, K4, GL, and S4, as well as all logics inheriting their admissible rules, have independent bases of admissible rules. 

Default logic is one of the most popular and successful formalisms for nonmonotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proofcomplexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen’s system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds (...) 

We develop canonical rules capable of axiomatizing all systems of multipleconclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [37]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumptionfree rule. Other applications of canonical rules include a generalization of the Blok–Esakia (...) 



We give proofs of the effective monotone interpolation property for the system of modal logic K, and others, and the system IL of intuitionistic propositional logic. Hence we obtain exponential lower bounds on the number of prooflines in those systems. The main results have been given in [P. Hrubeš, Lower bounds for modal logics, Journal of Symbolic Logic 72 941–958; P. Hrubeš, A lower bound for intuitionistic logic, Annals of Pure and Applied Logic 146 72–90]; here, we give considerably simplified (...) 