slideshow 3

Logic seminar

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

Propositional branching program proofs and logics for L and NL

Sam Buss
University of California, San Diego
Monday, 14. December 2020 - 15:30 to 17:00
Zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join
We introduce systems of propositional logic for reasoning directly with decision trees, non-deterministic decision trees, branching programs and non-deterministic branching programs. These propositional systems allow reasoning about properties in non-uniform logarithmic space and non-deterministic logarithmic space. We also report on work-in-progress to use these propositional proof systems for the bounded arithmetic theories VL and VNL with proof theoretic strength corresponding to logarithmic space and non-deterministic logarithmic space. The talk will start with an overview of the propositional proof systems which are already known to have close correspondences with bounded arithmetic. The new results are joint work with Anupam Das and Alexander Knop.

Interactive theorem proving for the working logician

Jeremy Avigad
Carnegie Mellon University
Monday, 7. December 2020 - 15:30 to 17:00
Zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join
Over the last few decades, computational proof assistants have made it possible to construct formal axiomatic derivations of increasing complexity. They are now used to verify that hardware and software designs meet their specifications, as well as to verify the correctness of mathematical proofs. The practice has taken root and promises to play an important role in mathematics and computer science.

In this talk, I will survey the technology, with an emphasis on formal mathematics. I will then discuss aspects of interactive theorem proving that may be of interest to the working logician, and places where a better theoretical understanding can lead to progress. Specifically, I'll discuss the need for practical foundations, search procedures, decision procedures, and proof systems.

Pages