JAIST Spring School 2012

• Nao Hirokawa: After an introduction to SAT and propositional encoding techniques, we discuss how to automatically analyse termination of term rewrite systems, which are considered as an abstract model of functional programs like Haskell or OCaml.
• Christian Sternagel: Following a brief introduction to the proof assistant Isabelle/HOL (including its underlying logic), we show how a formally verified certifier together with an external termination tool can be used to automatically obtain termination proofs of Isabelle/HOL functions.
• Mizuhito Ogawa: He talks on polynomial equality/inequality constraints solving on real (algebraic) numbers, which is shown to be decidable by Tarski in 1930's. We overview QE-CAD (Cylindrical Algebraic Decomposition) algorithm by Collins, 1975, and briefly mention the tool status in the field.

In proof analysis, axioms are converted into rules by which purely logical calculi are extended. The strongest results are usually obtained through extensions of contraction-free sequent calculi. Large classes of axioms are known by today that can be converted to such rules. For each of these classes, it is shown that central structural results of the purely logical calculus are maintained: closure under substitution and admissibility of weakening, contraction, and cut. The possibility to eliminate contraction, especially, often leads to systems with terminating root-first proof search.

This lecture begins with an overview of the background of proof analysis, then presents in increasing order of generality classes of axiomatic systems that can be turned into cut- and contraction-free sequent systems. As the main topic, proof analysis for labelled sequent calculi is presented. The labels are a formal notation for the possible worlds of Kripke semantics and result in a conservative extension of the logical syntax. The method provides analytic proof systems for wide classes of non-classical logics, including substructural logics, intermediate logics, classical and intuitionistic modal logics, provability logic, epistemic logics, conditional logics, and systems with dynamic and aggregation attitudes.

The way these calculi answer the challenge of extending proof-theoretic semantics to non-classical logics is also discussed, as well as their expressive power, analyticity, applicability to proof search, and their use in the solution of problems that usually involve complex model-theoretic constructions such as negative results in correspondence theory and modal embeddings among different logics. Finally, it is shown how direct completeness proofs, without artificial Henkin-set constructions, can be obtained with this methodology.

We start this lecture with an introduction to minimal logic, constructive (or intuitionistic) logic and classical logic through corresponding natural deduction systems, and with several examples of proofs which highlight differences among those logics.

We will review the well known translations, the Goedel-Gentzen negative translation, Kolmogorov's negative translation and Kuroda's negative translation, from classical logic into minimal or intuitionistic logic. The conservative extension result of classical logic over minimal logic with respect to negative formulas is given using the Goedel-Gentzen negative translation. We will also see Leivant's generalization of the result and variant of the generalization between classical logic and intuitionistic logic.

A variant of the Goedel-Gentzen translation will be introduced, and the class of formulas, for which classical logic is conservative over intuitionistic logic, is given. We will give some applications of this result for Barr's theorem and first-order arithmetic.

We will also introduce sequent calculi for intuitionistic logic and classical logic to analyze proofs of those logics in details. An analysis gives yet another conservative extension result of classical logic over intuitionistic logic.

The study of modal logics usually centres around a number of recurring questions, including completeness (``are all valid statements derivable?''), decidability (``is the logic amenable to automated reasoning?''), complexity (``what resources are required to mechanise the logic?'') and compositionality (``how do different logical features interact?'').

Coalgebraic Logics provide a uniform framework to address these questions which are typically studied on a per-logic basis. Without committing to a particular logic, the use of coalgebraic semantics allows for uniform proofs of completeness, decidability and complexity of many structurally different modal logics. Results about particular logics are then obtained as appropriate instantiations of the general framework. In this way, we not only derive results and algorithms for normal modal logics, but cover at the same time a large class of non-normal logics, including e.g. coalition logic, graded modal logic, probabilistic modal logic and majority logic. Moreover, coalgebraic techniques allow for the modular construction both of logics and their semantics: adding probabilities to coalition logics results in a logic of games with quantitative uncertainty. Similarly, different combinations of Hennessy-Milner logic and probabilistic modal logics can be used to describe various different types of probabilistic transition systems -- with completeness and decidability following from the modularity of the coalgebraic approach.

The lectures will present an overview of the state-of-the-art in coalgebraic logics and discuss modelling, reasoning, complexity and compositionality of coalgebraic logics.

In this lecture, I will give an overview of natural language semantics in terms of logic. Various phenomena of natural language have been explained by logic: e.g., tense and aspect, knowledge and belief, negation, implicature, anaphora, counterfactuality, and so on.

First, we shortly look back Montague semantics, the first distinguished achievement of logical representation of natural language semantic, including Categorial Grammar, Typed Lambda Calculus, and Intensional Logic. Also, we show Discourse Representation Theory and Mental Space, which explain the scope of our belief, anaphora, and negation. Thereafter, I will introduce the logic of multiple agents, in which knowledge and belief are represented by modal operators. Furthermore, I show the current stage of the logic of agent communication.

One of the noteworthy recent theories for semantics is hybrid logic, which extends modal logic with syntactic names of states called nominals, and overcomes some expressive weakness of the ordinary modal and tense logic. We will illustrate i) how hybrid logic allows us to formalize tense expressions including `until', `since', `then"; ii) how it realizes Reichenbach's analysis of tense; iii) how it can define some modally undefinable properties like irreflexivity, etc. Second, we overview a recent method of combining two hybrid logics, i.e., a method of handling two dimensions (e.g. time and space) at the same time in one setting.

In this tutorial I will give a gentle introduction to program extraction from proofs. We will study a proof calculus for constructive (or intuitionistic) first-order logic and show that, based on ideas of Kleene and Kreisel, one can extract from every proof a program that "realizes" the proven formula, that is, the program solves the computational problem expressed by the formula. In addition, one obtains a proof that the extracted program is indeed a correct solution to the problem. Hence, program extraction is a method for program generation and verification at the same time.

We will discuss some applications, mainly in constructive analysis, and demonstrate some tools for carrying out program extraction in practice implemented in the proof systems Minolg (Schwichtenberg) and Coq (Letouzey).

If time permits we will also look into other methods for extracting useful information from proofs, most notably, the Friedman/Dragalin method for extracting programs from classical, that is, nonconstructive, proofs, and a monotone version of Goedel's Dialectica Interpretation for extracting bounds in approximation and fixed point theory (Kohlenbach).

Term rewrite systems are a simple but general model of computation. Confluence is a property of rewrite systems that ensures results (normal forms) to be unique. In recent years, there is increased interest in automatically proving confluence and non-confluence of TRSs, with a number of actively developed tools (ACP, Saigawa, ...).

In this talk I will give an overview of confluence criteria employed in our tool, CSI, and demonstrate how proving confluence is related to rewriting equational proofs into so called valley proofs.

Pure Type Systems (or PTS) are a generic framework which allow to deal with several systems (Simply Typed Lambda Calculs, System F, Calculus of Constructions,...) all at once. Those systems mostly rely on an untyped notion of equality called conversion, which is based on program evaluation. To prove some theoretical properties of those systems, like their consistency in presence of external axioms, we may need to type the process of evaluation, leading to the notion of PTS with "judgmental equality".

However the theory behind this typed equality is strangely difficult to establish: the proofs of Confluence, Subject Reduction or Injectivity of Products are all linked together in a circular dependency. In this talk, I'll do a survey of the several result towards proving this equivalence, from Adams' first proof for functional PTS to my own PhD work which extends this result to *all* PTS. This result involves the description of a third "intermediate" system we called PTS with annotated typed reduction, which has all the necessary information to derive properties of PTS, even with a typed conversion.

The earliest proofs of the consistency of Peano arithmetic were presented by Gentzen, who worked out a total of four proofs between 1934 and 1939. In his best known proof from 1938 he gives a reduction procedure for derivations of the empty sequent, which represents a contradiction in the system. The proof shows that if there exists a derivation of the empty sequent, then there exists another less complex derivation, and another derivation, etc. He uses a height-line argument to construct the less complex derivations. It will be shown that the height-line construction is possible to avoid by a Howard-style vector assignment, which makes the reductions resemble proofs of direct cut elimination without multicut.

By iterating the powerset operation, the cumulative von Neumann hierarchy partitions the set theoretic universe into a union of sets, indexed by the ordinals. This description of the universe is a basic ingredient underlying a large part of proofs and conceptions of classical set theory.

However, considering set theories with constructive instead of classical logic which lack the powerset axiom (e.g. CZF instead of ZF), the potency of the hierarchy is severely reduced as its stages cannot be proved to be sets without using the principle of the excluded middle. This talk proposes a modified hierarchy and aims at demonstrating its validity by showing how its consequences for the role of ordinals in constructive set theory can be harnessed to obtain new results.

Three important results about the expressivity of a modal logic L are the Characterization Theorem (that identifies L as a fragment of a better known logic), the Definability theorem (that provides conditions under which a class of L-models can be defined by a formula or a set of formulas of L), and the Separation Theorem (that provides conditions under which two disjoint classes of L-models can be separated by a class definable in L).

In this talk I will show general conditions under which these results can be established for a given choice of model class and modal language whose expressivity is below first order logic. Besides some basic constrains that most modal logics easily satisfy, the fundamental condition that we require is that the class of omega-saturated models in question has the Hennessy-Milner property with respect to the notion of observational equivalence under consideration.