slideshow 3

Logic seminar

usually takes place each Monday at 14:00 in IM, rear building, ground floor
Chair: Pavel Pudlak, Neil Thapen
More information on the old seminar web page. The programme is announced via the mailing list.

An exponential lower bound for lengths of proofs in substructural logics

Raheleh Jalali Keshavarz
Institute of Mathematics
Monday, 23. September 2019 - 13:30 to 15:00
In this talk, we will investigate the lengths of proofs in the usual Gentzen calculus for the substructural logic FL_e. We will present a sequence of tautologies of the system and show any short proof for them implies a short proof for Hrubes' formulas for intuitionistic logic, hence the exponential lower bound follows. We will then conclude that this lower bound also applies to any proof system for a logic between FL_e and IPC.

Bounded-depth Frege complexity of Tseitin formulas for all graphs

Nicola Galesi
University of Rome Sapienza
Monday, 16. September 2019 - 13:30 to 15:00

We prove that Tseitin formulas Ts(G), for an undirected graph G, require proofs of size 2^{tw(G)^{\Omega(1/d)}} in depth d-Frege systems for d<{K \log n}/{\log \log n}, where tw(G) is the treewidth of G and K a constant. If time will allow, we prove tightness of the lower bound. Namely, that for large enough d, there are depth d-Frege proofs for Ts(G) of size 2^{\tw(G)^{\O(1/d)}} \poly(|Ts(G)|).This is a joint work with Dmitry Itsykson, Artur Riazanov and Anastasia Sofronova

Complexity of admissible rules with parameters

Emil Jeřábek
Institute of Mathematics
Monday, 27. May 2019 - 13:00 to 14:30
A rule \phi_1, ..., \phi_k / \psi is admissible in a (nonclassical) propositional logic L if the set of L-tautologies is closed under substitution instances of the rule. We are particularly interested in the set-up with parameters (constants), which are required to be preserved by substitutions. In this talk, we shall study basic properties of admissibility with parameters in a class of well-behaved transitive modal logics (i.e., extensions of K4). The main goal is a classification of the computational complexity of admissibility (and the closely related problem of unifiability) with parameters based on semantic properties of logics.

Propositional proofs and monotone computations

Pavel Pudlák
Mathematical Institute
Monday, 20. May 2019 - 13:00 to 14:30
One of the major discoveries of Stephen Cook is that lower bounds on the lengths of proofs in the propositional calculus can be used to prove independence results. This stimulated research into proving lower bounds for various propositional proof systems. Later it was shown that one can use lower bounds on the size of monotone circuits to prove lower bounds on propositional proofs. New models of monotone computations have been proposed recently that potentially may give us lower bounds for more propositional proof systems that we have so far. In this talk we will survey some results that connect lower bounds on monotone computations in various models with lower bounds on the lengths of proofs in proof systems.