The conference is composed of three invited keynote courses, and contributed talks. The invited courses, with the duration of three hours each, are organized in three sessions of one hour. The contributed talks will have the duration of twenty five minutes including discussion. Here you can find the pdf of the Program and the Booklet of Abstracts .
Invited keynote courses:
- Deirdre Haskell (Department of Mathematics and Statistics McMaster University, Canada):
Title: Some applications of model theory to algebra.
Abstract: I will assume a basic knowledge of logic, including completeness and compactness of first-order logic. Building on this, I will explore the notions of model completeness and quantifier elimination from a model-theoretic point of view, and discuss applications to theories of fields.
Lecture 1:
Model-theoretic criteria for model-completeness and quantifier elimination, with an application in real closed ordered fields.
Lecture 2:
Proof of quantifier elimination for real closed ordered fields and algebraically closed valued fields.
Lecture 3:
Elimination of imaginaries as seen in real closed ordered fields and algebraically closed valued fields.
- Wafik Lotfallah (The American University in Cairo, Egypt)
Title: The Power of Generalized Quantifiers in Finite (and Infinite) Model Theory.
Abstract: In the context of finite model theory and descriptive complexity, first order logic is known to have severe limitations. On one hand it cannot count, because very simple linear time queries such as Even (= Does the model have even size?) are not first order definable. On the other hand, it lacks recursion, because it cannot express some simple NLOGSPACE queries such as Reachability (= Is there a directed path from x to y?). To overcome these limitations, we could use infinitary logic, which allows infinite conjunctions and disjunctions. However, infinitary logic is too powerful, as it expresses all possible queries over the class of finite models. Thus, we could weaken this logic by insisting that the number of variables used in formulas is finite. This results into an interesting logic that can express recursion, but still lacks the power to count. Another alternative is to use second order logic, which is also quite powerful as it captures the polynomial hierarchy. In fact, even existential second order logic captures NPTIME. Thus, unless PTIME = NPTIME we need to seek weaker fragments of it. Still another approach is to augment first order logic with counting quantifiers (that count) and/or fixed point operators (that express recursion). These different ways of extending first order logic are two instances of the generalized quantifiers, introduced by Lindström in 1966. This minicourse motivates the introduction of generalized quantifiers and illustrates their power and limitation. It is assumed that the audiences are familiar with first order logic and basic model theory, as well as few notions from complexity theory, e.g. PTIME. The course stresses on basic concepts, examples, and proof ideas. Below is an outline of the lectures:
Lecture 1: Basic Definitions and Motivation: • Limitations of first order logic • Infinitary logic (with finitely many variables), (existential) second order logic • Fixed point logic • Counting quantifiers, unary quantifiers • Generalized quantifiers, arity, width, and type • Examples (lecture notes: pdf (1.5MB))
Lecture 2: Games Capturing Logics: • Ehrenfeucht games for first order logic, applications • Pebble games for infinitary logic, applications • Bijective games for logics with generalized quantifiers of bounded arity (lecture notes: pdf (1.4MB))
Lecture 3: Hierarchy Theorems for Generalized Quantifiers: • Type hierarchy • Quantifier rank hierarchy • Lower bounds for expressive power
References: 1) Ebbinghaus and J. Flum: Finite Model Theory, 2nd Edition, Springer Verlag, Chapter 12, (1999). 2) Hella: Logical hierarchies in PTIME, Information and Computation, vol. 129, pp. 1-19 (1996). 3) Hella, Luosto, and Väänänen: The Hierarchy Theorem for Generalized Quantifiers, Journal of Symbolic Logic, vol. 61, pp. 802-817 (1996). 4) Keisler and Lotfallah: Rank Hierarchies for Generalized Quantifiers, submitted to the Annals of Pure and Applied Logic, preprint available from the authors. 5) Lindström: First order predicate logic with generalized quantifiers, Theoria, vol. 32, pp. 186–195 (1966). 6) Väänänen: A survey of generalized quantifiers on finite models, from Väänänen’ website: http://www.math.helsinki.fi/logic/opetus/ylkvantII/beatcs.pdf
- Simão Melo de Sousa (Departamento de Informática, Universidade da Beira Interior, Portugal):
Title: An introduction to program logic and the formal development of software.
Abstract: In these three lessons, I will motivate and give a short overview of the
formal development of software. In particular I will expose how the
seminal ideas of Hoare, Floyd, Dijkstra gave rise to two rich methodologies
(and subsequent tools) for the design of correct software: the Design
by Contract approach and the Model based Software Design approach.
For this last, I will follow the B Method.
Plan:
Lecture 1:
- The need for a rigourous (logical) approach to the software
development approach and
- an introduction to the formal development of software
Lecture 2: Hoare Logic and the Design by Contract paradigm
-
Lecture 3: From Hoare triples and predicate transformers to generalized
substitutions: the B Method approach
|
|