Embedded Files
ABSTRACTS
Lorenza Carlucci (MAT-Sapienza)
Talk: Reverse mathematics and computable analysis of combinatorial principles
Abstract: Mathematical logic offers sophisticated tools to compare theorems accordings to their axiomatic or computational strength. I will give a general overview of this kind of research with a focus on combinatorial theorems from Ramsey theory.Giuseppe De Giacomo (CS-OXford & DIAG-Sapienza)
Talk: Temporal synthesis in Linear Temporal Logic for finite and infinite traces
Abstract: Temporal synthesis is an area of Formal Methods that studies how to automatically synthesize interactive programs from a human-readable specification, typically expressed in temporal logic. Temporal synthesis is deeply related to planning for temporally extended goals in AI. In this talk, we will focus on Linear Temporal Logic on finite traces that has emerged as a particularly interesting logic for decision making in autonomous AI systems. Technically, a key advantage of working in the finite-trace setting is its simplicity, due to reducibility to regular automata, which can be easily determinized and transformed into two-player games on graphs. This simplicity leads to an unprecedented computational effectiveness and scalability of synthesis when compared to Linear Temporal Logic on infinite traces. We then discuss some recent results on how to lift this finite-trace "technology" to infinite traces by leveraging Manna and Pnueli’s safety-progress hierarchy for temporal properties, which is ultimately based on a finite-trace core.Nicola Galesi (DIAG-Sapienza)
Talk: The complexity of logical proofs and the P vs NP problem
Abstract: In a milestone paper of '74 Cook and Reckhow showed that NP = coNP is equivalent to show that there exists a proof system where any tautology formula F admits a proof of size (its length as a string) at most polynomial in the size of F itself. A proof system holding this property was called "super". Since NP≠coNP implies that P≠NP, the theorem suggested a strategy to attack the latter result: proving that there is no super proof systems at all. Of course such a result is out of reach of the current mathematical techniques. However Cook suggested the following strategy to attack it, known as "Cook's program towards P≠NP": starting from the simplest, weakest and concrete examples of proof systems, prove they are not "super" and go on with stronger and stronger (from the point of view of proving tautology efficiently) proof systems, until we will have sufficient mathematical knowledge and techniques to attack the universal full problem. It turned out that even proving that a simple propositional proof system like Resolution was a hard task and took around ten years after Cook-Reckhow's paper to prove that Resolution is not super. Nowadays Cook's Program greatly advanced and established proof complexity - the field that studies the complexity of proving tautologies - as an independent field with a lot of interesting connections with other theoretical and applied fields related to Computer Science. Nevertheless proving that text-book propositional systems like Hilbert axiomatic systems or Gentzen Sequent Calculus are not super is, at the moment, unknown and out of reach of current techniques.In the talk I will give a brief introduction to Proof Complexity aimed at understand what does it mean precisely to prove that a proof system is not super. I will introduce the main ideas used to prove that a restriction of Resolution is not super as an example ofthe hardness of proving such results.
Massimo Lauria (DSS-Sapienza)
Talk: SAT-Solvers
Abstract: SAT-solvers are programs to solve the satisfiability problem (SAT), that is to decide whether a propositional formula admits or not a satisfying boolean assignment. SAT is the root problem among the NP-complete problems and as such is conjectured not to be solvable efficiently.In the talk I'll give an accessible introduction to the main algorithms which are at the core of the modern and most efficient SAT-solvers. Despite the computational hardness of SAT, modern SAT-solvers are able to solve quite efficiently instances of SAT for formulas encoding industrial and applied problems involving hundreds of thousands of variables.
SAT-solvers also produce a proof of their correctness, which can be therefore efficiently verified. Such an aspect allows a deep analysis of their computational limitations through the lens of proof complexity, that is the study of the complexity of logical proofs.
PROGRAM
9:00 - 9:40 Maurizio Lenzerini - Logic in Databases
9:45 - 10:15 Massimo Lauria - SAT-Solvers
10:20 - 10: 50 Giuseppe De Giacomo - Temporal synthesis in Linear Temporal Logic for finite and infinite traces
10:55 - 11:10 Break
11:15 - 11:45 Nicola Galesi - The complexity of logical proofs and the P vs NP problem
11:50 -12:20 Lorenzo Carlucci - Reverse mathematics and computable analysis of combinatorial principles
Page updated
Report abuse