# 6th Panhellenic Logic Symposium

Volos, Greece, 5-8 July 2007

### 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).