Programme
Thursday 5.7.07
- 09:00-10:00
- Registration - Opening
- 10:00-11:00
- Constantine Tsinakis (Vanderbilt University):
- Algebraic Methods in Logic
Algebraic logic studies classes of algebras that are related to logical systems,
as well as the process by which a class of algebras becomes the algebraic
counterpart (semantics)" of a logical system. A field practitioner usually
approaches the solution of a problem in logic by first reformulating it in
the language of algebra; then by using algebra to solve the reformulated problem;
and lastly by expressing the result into the language of logic. A representative
association of the preceding kind is the one between the class of Boolean algebras
and classical propositional calculus.
The focus of this talk is substructural logics and their algebraic counterparts.
Substructural logics are non-classical logics that are weaker than classical logic,
in the sense that they lack one or more of the structural rules of contraction,
weakening and exchange in their Genzen-style axiomatization. (It is, however,
convenient to think of the classical logic and intuitionistic logic as substructural
logics.) These logics encompass a large number of non-classical logics related to
computer science (linear logic), linguistics (Lambek Calculus), philosophy
(relevant logics), and multi-valued reasoning.
The following are among the objectives of the talk:
Propose a uniform framework for the study of the algebraic counter-parts of
substructural propositional logics. These algebras, referred to as residuated
lattices, have a recently discovered rich structure theory. (Note: The term
"residuated lattice" has been used in the literature to refer to
algebras that are integral, commutative and bounded. This class and its
subclasses are not sufficiently general to provide semantics for all
substructural logics.)
Show how the algebraic theory of residuated lattices can produce powerful
tools for the comparative study of substructural logics.
Stress that the bridge algebraic logic builds is beneficial to both algebra
and logic, and that an in depth study of residuated lattices is impossible
without the use of logical and proof-theoretic techniques. This point is
illustrated with a discussion of the close connection between interpolation
theorems for a substructural logic and the amalgamation property for its
algebraic counterpart.
- 11:00-11:30
- Long Coffee Break
- 11:30-12:30
- Sergei Artemov (City University of New York):
- Justification Logic
We describe a formal theory of justification, Justification Logic, based on classical
propositional logic augmented by justification assertions t:F that reads "t is a
justification for F." Justification Logic assumes certain justification principles
originating from both the mathematical theory of proofs and mainstream epistemology.
Lecture 1 will be devoted to the Logic of Proofs LP which gives a propositional
axiomatization of proof assertions t:F read as "t is a proof of F" and shows that there
is a hidden explicit witness (proof) structure behind S4 and other classical modal
logics. This may be regarded as a completion of Kolmogorov and Goedel's effort of the
early 1930es to explain intuitionistic logic using the classical notion of proof.
Lecture 2 will extend this technique to the general purpose Justification Logic, which is
a family of logical systems capturing the notion of justification supplied with Fitting's
epistemic semantics. We apply Justification Logic for analyzing Plato's celebrated
definition of Knowledge as Justified True Belief.
- 12:30-13:30
- Ayse Berkman (Middle East Technical University):
- Groups of Finite Morley Rank
I shall make a quick introduction to the subject, give examples and present the
Borovik program that shaped around the main conjecture of the area:
Algebraicity Conjecture
An infinite simple group of finite Morley rank is isomorphic to
an algebraic group over an algebraically closed field.
In the second half of my talk, I shall present some recent results
from the study of groups of finite Morley rank with pseudoreflection subgroups:
If G acts on an abelian group V, with an infinite definable connected abelian subgroup R
such that V=[V,R] ⊕ CV(R) and R acts transitively on the non-zero elements of
[V,R], then R is called a pseudoreflection subgroup of G.
- 13:30-17:00
- Lunch Break
- 17:00-17.25
- Konstantinos Pouliasis and Nikolaos S. Papaspyrou:
- Axiomatizing Principia Metaphysica in Isabelle/HOL
- 17:25-17.50
- Michalis A. Papakyriakou, Prodromos E. Gerakios and Nikolaos S. Papaspyrou:
- A Mechanized Proof of Type Safety for the Polymorphic ë-Calculus with References
- 17:50-18.15
- Vladimir Sotirov:
- Leibniz's "Calculemus!" at Work
- 18:15-18.40
- Svetla Koeva, Tinko Tinchev and Mitko Yanchev:
- Decidability of generalized majority logic
- 18:40-19.00
- Coffee Break
- 19:00-19.25
- Walter Dean:
- On Moschovakis's theory of algorithmic identity
- 19:25-19.50
- Nikolaos Galatos:
- Algebraic and Relational Semantics for Substructural Logics
- 19:50-20.15
- Yiorgos Stavrinos and Anastasia Veneti:
- Of kits and molecules
Friday 6.7.07
- 09:00-10:00
- Sergei Artemov (City University of New York):
- Justification Logic
We describe a formal theory of justification, Justification Logic, based on classical
propositional logic augmented by justification assertions t:F that reads "t is a
justification for F." Justification Logic assumes certain justification principles
originating from both the mathematical theory of proofs and mainstream epistemology.
Lecture 1 will be devoted to the Logic of Proofs LP which gives a propositional
axiomatization of proof assertions t:F read as "t is a proof of F" and shows that there
is a hidden explicit witness (proof) structure behind S4 and other classical modal
logics. This may be regarded as a completion of Kolmogorov and Goedel's effort of the
early 1930es to explain intuitionistic logic using the classical notion of proof.
Lecture 2 will extend this technique to the general purpose Justification Logic, which is
a family of logical systems capturing the notion of justification supplied with Fitting's
epistemic semantics. We apply Justification Logic for analyzing Plato's celebrated
definition of Knowledge as Justified True Belief.
- 10:00-11:00
- Stuart Barry Cooper (University of Leeds):
- The Interactive Structure of Information: Post's Program Revisited
Computability theory concerns information with a causal structure. As such,
it provides a schematic analysis of many naturally occurring situations.
Emil Post was the first to focus on the close relationship between information,
coded as real numbers, and its algorithmic infrastructure. Having characterized
the close connection between the quantifier type of a real and the Turing jump
operation, he looked for more subtle ways in which information entails a particular
causal context. Specifically, he wanted to find simple relations on reals which
produced richness of local computability-theoretic structure. To this extent,
he was not just interested in causal structure as an abstraction, but in the way
in which this structure emerges in natural contexts. "Post's program" was the
genesis of a more far reaching research project.
In this talk we will firstly review the history of Post’s program, and look at
two interesting developments of Post’s approach. The first of these developments
concerns the extension of the core program, initially restricted to the Turing
structure of the computably enumerable sets of natural numbers, to the Ershov
hierarchy of sets. The second looks at how new types of information coming
from the recent growth of research into randomness, and the revealing of
unexpected new computability-theoretic infrastructure. We will conclude by
viewing Post's program from a more general perspective. We will look at how
algorithmic structure does not just emerge mathematically from information,
but how that emergent structure can model the emergence of very basic aspects
of the real world.
- 11:00-11:30
- Long Coffee Break
- 11:30-12:30
- Ilijas Farah (York University):
- Set Theory and the Calkin Algebra
Calkin algebra is the 'quantized' analogue of the Boolean algebra
P(N)/Fin. Analogues of well-known theorems about P(N)/Fin are sometimes
well-known open problems about the Calkin algebra. Solving them requires
a fresh look at the old proofs. I am going to survey some of the recent
results.
- 12:30-13:30
- Thomas Eiter (Vienna University of Technology):
- Towards a Semantic Web: Combining Rules and Ontologies
In the last years, there have been increasing efforts to bridge the separated
worlds of rule-based formalisms and of logic-based ontology languages for
knowledge representation and reasoning. This is in particular motivated
by the vision of an enhanced version of the World Wide Web, in which semantic
access to contents is provided for machine-based information processing.
While ontologies play here a key role, the most prominent formalisms and
standards including the Resource Description Framework (RDF) and the Web
Ontology Language (OWL), which is based on description logics, are insufficient
to accommodate the needs for knowledge representation in practice. Several
proposals for combining rule and ontology formalisms have been made so far,
which differ in various respects. However no generally agreed upon solution
to the problem has been found so far (and may not exist). In this talk,
we address some approaches to combine rules and ontologies, and the problems
which arise in this task. Special emphasis is given to non-monotonic combinations
that are capable of dealing with missing information, which appears to be a necessary
feature for advanced reasoning on the Web. The talk will conclude with some issues
for future research.
- 13:30-17:00
- Lunch Break
- 17:00–17:25
- Vassilis Kountouriotis, Christos Nomikos and Panos Rondogiannis:
- Boolean Grammars and Negation in Logic Programming
- 17:25-17:50
- Anton Zinoviev:
- Logical Applications of the Dual Boolean Ring
- 17:50-18:15
- Eleni Kalyvianaki:
- Locality and its applications in natural language semantics
- 18:15-18:40
- Pedro Cabalar, David Pearce and Agustin Valverde:
- Minimisation of logic programs
- 18:40:19:00
- Coffee Break
- 19:00-19:25
- Alexander Sakharov:
- Classicality as a Property of Predicate Symbols
- 19:25-19:50
- Konstantinos Georgatos:
- Geodesic Update
- 19:50-20:15
- Anastasios Michael Fotinopoulos and Pavlos Peppas:
- Connecting Recovery and Iterated Belief Revision
Saturday 7.7.07
- 09:00-10:00
- Ilijas Farah (York University):
- Set Theory and the Calkin Algebra
Calkin algebra is the 'quantized' analogue of the Boolean algebra
P(N)/Fin. Analogues of well-known theorems about P(N)/Fin are sometimes
well-known open problems about the Calkin algebra. Solving them requires
a fresh look at the old proofs. I am going to survey some of the recent
results.
- 10:00-11:00
- Anuj Dawar (University of Cambridge):
- On Preservation Theorems in Finite Model Theory
Among classical theorems of model theory, preservation theorems are results that
relate the syntactic form of formulas to semantic closure properties of the
structures they define. The status of preservation theorems in the finite has
been an active area of research in finite model theory. More recent work in the
area has shifted the focus from the class of all finite structures to classes of
structures satisfying natural structural restrictions. In this talk I will examine
various recent results relating to preservation under homomorphisms and extensions,
both on the class of all finite structures and on more restricted classes.
- 11:00-11:30
- Long Coffee Break
- 11:30-12:30
- Silvio Ghilardi (University of Milano):
- Model-theoretic techniques for combined decision procedures in word problems, constraint satisfiability, and model-cheching
In various areas of Logic, Software Verification and Artificial
Intelligence, specific formalisms and inference mechanisms are often
needed. Such formalisms are able to treat decision problems (modulo a
particular theory) for relevant fragments of a logical language or, more
generally, to treat satisfiability problems for various kinds of
constraints. In order to be concretely useful, such quite specific
formalisms must be integrated within each other and within suitable
'general purpose' deductive systems dealing for instance with elementary
or higher order logic. The need of such an integration gives rise to a
specific area in Automated Reasoning: the main task in this area is the
modular combination of the enormous amount of knowledge, specific procedures
and deductive systems already well-known to the scientific community.
In this mini-course on combination of decision procedures, we review
(taking a model-theoretic viewpoint) recent developments concerning
decidability transfer results: we recall the basic Nelson-Oppen schema
known since 1980, and we see how it can be extended to non-disjoint
signatures and to quite elaborated logical formalisms. While keeping
model-completeness and quantifier-elimination as the main conceptual
tools, we traverse in a uniform way various applications domains, ranging
from algebraic equational reasoning, to universal fragments of first-order
theories, to modal/description logics, and finally also to model-checking
for infinite state systems (where adding a temporal dimension to a first
order theory is treated as a special kind of a combination problem).
- 12:30-13:30
- Michalis Mytilineos: In memoriam
- 13:30-20:00
- Excursion
Sunday 8.7.07
- 09:00-10:00
- Silvio Ghilardi (University of Milano):
- Model-theoretic techniques for combined decision procedures in word problems, constraint satisfiability, and model-cheching
In various areas of Logic, Software Verification and Artificial
Intelligence, specific formalisms and inference mechanisms are often
needed. Such formalisms are able to treat decision problems (modulo a
particular theory) for relevant fragments of a logical language or, more
generally, to treat satisfiability problems for various kinds of
constraints. In order to be concretely useful, such quite specific
formalisms must be integrated within each other and within suitable
'general purpose' deductive systems dealing for instance with elementary
or higher order logic. The need of such an integration gives rise to a
specific area in Automated Reasoning: the main task in this area is the
modular combination of the enormous amount of knowledge, specific procedures
and deductive systems already well-known to the scientific community.
In this mini-course on combination of decision procedures, we review
(taking a model-theoretic viewpoint) recent developments concerning
decidability transfer results: we recall the basic Nelson-Oppen schema
known since 1980, and we see how it can be extended to non-disjoint
signatures and to quite elaborated logical formalisms. While keeping
model-completeness and quantifier-elimination as the main conceptual
tools, we traverse in a uniform way various applications domains, ranging
from algebraic equational reasoning, to universal fragments of first-order
theories, to modal/description logics, and finally also to model-checking
for infinite state systems (where adding a temporal dimension to a first
order theory is treated as a special kind of a combination problem).
- 10:00-11:00
- Ali Enayat (American University):
- Automorphisms of Models of Arithmetic
We discuss a recently developed method of constructing automorphisms of models
of arithmetic that provides a unified, powerful approach to building desirable
automorphisms of models of a variety of arithmetical theories, ranging from bounded
arithmetic to second order arithmetic. As we shall explain, this new method can also
be used to establish a long standing conjecture of Schmerl by showing that the
isomorphism types of fixed point sets of countable arithmetically saturated model M
of Peano arithmetic are precisely the isomorphism types of elementary submodels of M.
- 11:00-11:30
- Coffee Break
- 11:30-11:55
- Dimiter Vakarelov:
- A recursive generalization of Ackermann Lemma with applications to modal ì-definability
- 11:55-12:20
- Alexandra A. Soskova and Ivan N. Soskov:
- Jump spectra of abstract structures
- 12:20-12:45
- Hristo Ganchev and Ivan Soskov:
- The groups AUT(Dù') and AUT(De) are isomorphic
- 12:45-13:10
- Georgi Georgiev:
- Quantifiers on equivalence relations in local agreement
- 13:10-13:35
- Alla Sirokofskich:
- Census Functions in Weak Arithmetic
