Home >  Programme

Invited Speakers

Marcelo Finger Algebraic Multipliers: a New Characterization of Validity for Classical and Many-Valued Logics
We propose a novel algebraic characterisation of the classical notion of validity in terms of boolean rings, called entailment multipliers. We demonstrate the existence of such multipliers and show how they can be used to derive stronger entailment statements. An interesting property of multipliers lies in their behaviour as invariants in a proof, a fact that is used to show how several inference systems can be employed to compute entailment multipliers. A similar characterisation of validity for modal logics is presented.

M. van Lambalgen Logical form as a determinant in cognitive processes. We discuss a research program on reasoning patterns in subjects with autism, showing that they fail to engage in certain forms of non-monotonic reasoning that come naturally to neurotypical subjects. The striking reasoning patterns of autists occur both in verbal and in non-verbal tasks. Upon formalising the relevant non-verbal tasks, one sees that their logical form is the same as that of the verbal tasks. This suggests that logical form can play a causal role in cognitive processes, and we suggest that this logical form is actually embodied in the cognitive capacity called 'executive function'.
Tutorial : Probabilistic reasoning is non-monotonic, but not all non-monotonic reasoning can be represented in probability theory. The book 'Bayesian rationality' by M. Oaksford and N. Chater (2004) contains the most sustained argument to date for the thesis that since ordinary reasoning must deal with uncertainty and hence with non-monotonicity, logic is useless in giving an account of how people actually reason. We show however that a prominent form of common sense non-monotonic reasoning, closed world reasoning, cannot be captured by probability theory. We will discuss the implications of this for currently popular 'dual process' theories of cognition.

Ian Pratt-HartmannLogics with Counting Quantifiers Counting quantifiers are expressions in formal languages having English glosses of the forms ``there exist at least/at most/exactly C objects x such that ... x ...'', where C is a natural number. In the context of first-order logic with equality, counting quantifiers have no effect on expressive power, since they can all be defined by means of universal or existential quantifiers in the familiar way. In the context of many *fragments* of first-order logic, however, adding counting quantifiers greatly increases expressive power; and it is of interest to understand the effects which this increased expressiveness has on various model-theoretic and complexity-theoretic properties of these fragments. This talk surveys the known results in this area. In particular, we consider the one- and two-variable fragments of first-order logic with counting quantifiers, modal logics with counting modalities and the guarded two-variable fragment of first-order logic with counting quantifiers. We round off---time permitting---with some (comparatively speaking) amusing facts about the numerical syllogistic.

Johann (Janos) A. Makowsky Interpretations of Combinatorial Sequences We discuss various classical results of N. Chomsky and Schuetzenbeger (1963), C. Blatter and E. Specker (1981), and I. Gessel (1984) about combinatorial sequences satisfying various recurrence relations. They all show that definability of the interpretations of these sequences in Monadic Second Order Logic is a sufficent, and sometimes also necessary condition for the existence of certain recurrence relations. We also discuss limitations and improvements of the Specker-Blatter Theorem due to E. Fischer (2003) and the speaker, and extensions of these results to holonomic sequences due to T. Kotek and the speaker.

Martin Lange A CTL-Based Logic for Program Abstractions

Sebastiaan A. Terwijn Computability theoretic interpretations of intuitionistic logic In this talk we discuss some of the more recent developments in the area between intuitionistic logic and the theory of computation, in particular the relation with the Medvedev and Muchnik lattices. In a sketchy paper, Kolmogorov suggested to interpret the intuitionistic propositional calculus $\IPC$ as a ``calculus of problems''. Later Medvedev investigated several ways in which this could be made precise, and introduced the lattice that now bears his name. Although initially this approach was unsuccessful in capturing $\IPC$, later work of Skvortsova showed that it could be made to work after all. We explain Skvortsova's result, which is a culmination of ideas from proof theory, lattice theory, and computability, and we discuss recent work with Sorbi about the extent of this approach.

Cesare Tinelli Foundations of Satisfiability Modulo Theories

Programme

WoLLIC 2010 Preliminary Programme

Tuesday, 6 July

 09.00 Michiel van Lambalgen (University of Amsterdam)
Tutorial: Probabilistic reasoning is non-monotonic, but not all
non-monotonic reasoning can be represented in probability theory -  Part 1
10:00 Coffee-break
10.30  Michiel van Lambalgen (University of Amsterdam)
Tutorial: Probabilistic reasoning is non-monotonic, but not all
non-monotonic reasoning can be represented in probability theory - Part 2
11:30 Short break
11.40 Sebastiaan Terwijn (Radboud University Nijmegen )
Tutorial 1: Intuitionistic Logic
12.40 Lunch
14.00 Marcelo Finger (IME /University of São Paulo)
Tutorial:  Satisfiability and Probabilistic Satisfiability - Part 1
15.00 Short break
15.10  Marcelo Finger (IME /University of São Paulo)
Tutorial:  Satisfiability and Probabilistic Satisfiability - Part 2
16.10 Coffee-break
16.40 Johann Makowsky (Technion - Israel Institute of Technology)
Tutorial:  Two lectures on the model theory of graph polynomials
Why is the chromatic polynomial a polynomial? - Part 1
17.40 close

Wednesday, 7 July

 09.00 Sebastiaan Terwijn (Radboud University Nijmegen )
Tutorial 2: Computability Theory
10:00 Coffee-break
10.30 Johann Makowsky (Technion - Israel Institute of Technology)
Tutorial:  Two lectures on the model theory of graph polynomials
Intriguing questions about graph polynomials - Part 2
11.30  Sven Hartmann and Thu Trinh (Clausthal University of Technology)
Solving the Implication Problem for XML Functional Dependencies with Properties
12.00 Naeem Abbasi, Osman Hasan and Sofiene Tahar (Concordia University)
Formal Lifetime Reliability Analysis Using Continuous Random Variables
12.30 Lunch
14.00 Marcelo Finger (IME /University of São Paulo)
Algebraic Multipliers: a New Characterization of Validity for  Classical and Many-Valued Logics
15.00  Andréia B. Avelar, Flavio de Moura, André Luiz Galdino and Mauricio Ayala-Rincon (University of Brasília)
Verification of The Completeness of Unification Algorithms à la Robinson
15.30 Coffee-break
16.00 Cesare Tinelli (University of Iowa)
Foundations of Satisfiability Modulo Theories
17.00 Aditi Barthwal and Michael Norrish (Australian National University)
Mechanisation of PDA and Grammar Equivalence for Context-Free Languages
17.30 close

Thursday,  8 July

 09.00 Ian Pratt-Hartman (University of Manchester)
Logics with Counting Quantifiers
10.00 Carlos Areces, Alexandre Denis and Guillaume Hoffmann (INRIA Nancy, TALARIS)
A Modal Logic with Counting
10.30 Coffee-break
11.00 Johann Makowsky (Technion - Israel Institute of Technology)
Application of Logic to generating functions: Proving recurrence  relations
12.00  Flavio Ferrarotti, Sven Hartmann and Sebastian Link (University of Wellington)
On the Role of the Complementation Rule for Data Dependencies over Incomplete Relations
12.30 Lunch
14.00 Michiel van Lambalgen (University of Amsterdam)
Logical form as a determinant in cognitive processes
15.00 Ramyaa Ramyaa and Daniel Leivant (Indiana University)
Feasible functions over coinductive data
15.30 coffee
16.00 Richard Zuber (CNRS Paris)
Generalising Conservativity
16.30 Glyn Morrill and Oriol Valentín (U. Politècnica de Catalunya e U. Pompeu Fabra)
The Binding Principles in Categorial Grammar
17.00 Daniele Nantes Sobrino and Mauricio Ayala-Rincon (University of Brasilia)
Reduction of the intruder deduction problem into equational elementary
deduction for electronic purse protocols with blind signatures
17.30 close

Friday, 9 July

 09.00 Sebastiaan Terwijn (Radboud University Nijmegen)
Comptability-theoretic interpretations of intuitionistic logic
10.00  Daniel Ventura, Mauricio Ayala and Fairouz Kamareddine (University of Brasilia, Heriot-Watt University)
Intersection type systems and explicit substitutions calculi
10.30 Coffee-break
11.00 Martin Lange (University of Kassel)
A CTL-Based Logic for Program Abstractions
12.00 Alexis Goyet, Yoshinori Tanabe and Masami Hagiya (Ecole Normale Supériore, University of Tokyo)
Decidability and undecidability results on the modal mu-calculus with
a natural number-valued semantics
12.30 Renata Reiser, Benjamin Bedregal and Gesner Dos Reis  Interval Valued Fuzzy Coimplication (Fed. Univ. Rio Grande do Norte, UCPel )
13.00 Lunch and close

Last modified: July 9, 2009, 11:01am GMT-3.