Invited Tutorials
- 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.
- 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.
- 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).
