SEMINAR ON LOGIC IN COMPUTER SCIENCE

Faculty of Mathematics and Computer Science
University of Bucharest


Now superseded by the unified FMI/IMAR Logic Seminar!






Coordinators (2014):
Claudia Chiriță, Andrei Sipoș

Seminar LCS 2013 (Archive)          Google group






06.06.2014, Amf. D. Pompeiu (FMI, UB), 10.00
Speaker:
Tommaso Flaminio (DiSTA, Università dell'Insubria)
Title: 
Non-standard methods in the theory of MV-algebras and states

Abstract:

Semisimple MV-algebras are, by Chang-Belluce theorem, algebras of continuous real-valued functions. Di Nola’s theorem, more in general, represents any MV-algebra as an algebra hyperreal-valued maps. This simple observation points out that, although methods from real analysis are enough to improve our knowledge on semisimple MV-algebras, as for non-semisimple ones, non-standard analysis seems to be the right setting to frame the investigation. In this seminar we apply methods from non-standard analysis to the representation of non-semisimple MV-algebras and state theory. In particular we show a uniform representation for MV-algebras which contains Chang-Belluce and Di Nola’s theorems as particular cases, and we introduce a variant of classical de Finetti’s coherence criterion in which players wager (a possibly infinitesimal amount of) money on the occurrence of a certain class of events which are hyperreal-valued maps.



30.05.2014, Amf. D. Pompeiu (FMI, UB), 10.00
Speaker: Denisa Diaconescu (FMI, UB)
Title: 
Stone-like dualities: a tool for generalizing finite automata

Abstract:

The aim of the seminar is to show how the finite slice of Stone duality can be used to define a dictionary for translating deterministic finite automata (thought as set-theoretical objects) in the language of classical propositional logic. By this translation, we obtain objects of classical propositional logic, called classical fortresses, which accept exactly the same languages as finite automata: regular languages. Classical fortresses allow easy generalizations to non-classical logics: given a propositional logical calculus L which is algebraizable, locally finite, and enjoys a Stone-like duality, one can adapt the definition of classical fortress to the framework of L, introducing a notion of L-fortress and studying the language accepted by such objects. We investigate the following question: What is the reflection of L-fortresses in the theory of automata? We explicit our method for Gödel logic.




22.05.2014, Amf. D. Pompeiu (FMI, UB), 14.00
Speaker: Laurențiu Leuștean (IMAR) 
Title: 
An invitation to proof mining II (Effective results on the mean ergodic theorem)

Abstract:

The program of proof mining is concerned with the extraction of hidden finitary content from proofs that make use of highly infinitary principles. The new information is obtained after a logical analysis, using proof-theoretic tools, and can be both of quantitative nature, such as algorithms and effective bounds, as well as of qualitative nature, such as uniformities in the bounds. This line of research, developed by Kohlenbach in the 90's, has its roots in Kreisel's program on unwinding of proofs, put forward in the 50's.
In this talk we give an overview of proof mining and its applications.




16.05.2014, Amf. D. Pompeiu (FMI, UB), 10.00
Speaker: Laurențiu Leuștean (IMAR) 
Title: 
An invitation to proof mining

Abstract:

The program of proof mining is concerned with the extraction of hidden finitary content from proofs that make use of highly infinitary principles. The new information is obtained after a logical analysis, using proof-theoretic tools, and can be both of quantitative nature, such as algorithms and effective bounds, as well as of qualitative nature, such as uniformities in the bounds. This line of research, developed by Kohlenbach in the 90's, has its roots in Kreisel's program on unwinding of proofs, put forward in the 50's.
In this talk we give an overview of proof mining and its applications.





25.04.2014, Amf. D. Pompeiu (FMI, UB), 10.00
Speaker: Andrei Sipoș (MSc student, FMI, UB) 
Title: A Choice of Basis: the softer side of independence

Abstract:

We show how a number of results around the Axiom of Choice can be proven to be equivalent.



11.04.2014, Room 214 (FMI, UB), 10.00
Speaker: Andrei Sipoș (MSc student, FMI, UB)
Title: Independence results in Peano arithmetic

Abstract: 
We sketch the proof of the fact that the termination of Goodstein sequences is not provable in first-order Peano arithmetic, following the original article by Kirby and Paris.

References:




04.04.2014, Amf. D. Pompeiu (FMI, UB), 10.00
Speaker: Claudia Chiriță (MSc student, FMI, UB) 
Title: Abstract representations of consequence (II)

Abstract: 
We discuss a number of abstractions of logical systems that build upon the concept of consequence rather than that of satisfaction. Our primary goal is to describe consequence in terms of derivability instead of the model theoretic notion of entailment provided by the theory of institutions. We further present the links between these views of consequence and how they can be put together in the form of institutions equipped with entailment systems.


28.03.2014, Amf. D. Pompeiu (FMI, UB), 10.00
Speaker: Claudia Chiriță (MSc student, FMI, UB) 
Title: Abstract representations of consequence

Abstract: 
We discuss a number of abstractions of logical systems that build upon the concept of consequence rather than that of satisfaction. Our primary goal is to describe consequence in terms of derivability instead of the model theoretic notion of entailment provided by the theory of institutions. We further present the links between these views of consequence and how they can be put together in the form of institutions equipped with entailment systems.

References:
http://link.springer.com/chapter/10.1007%2F3-540-50325-0_3#page-1






10.03.2014, Amf. D. Pompeiu (FMI, UB), 12.00
Speaker: Andrei Sipoș (MSc student, FMI, UB) 
Title:  What is Logic (in Computer Science)?

Abstract: 

We relaunch the seminar with an examination of the roles that logic and computer science can play in each other's development, e.g. by way of formal theorem-proving, verification or semantics, which will (hopefully) reveal the themes that would pervade the lectures throughout the year.