Workshop on Logic and Computation

— from proof theory to software verification —

February 8–9, 2011

Kanazawa, Japan

About the Workshop

The workshop aims at promoting interactions among logicians from proof theory, computability, and rewriting. The workshop is organised as an informal one, and not only presentations about published results but also about work in progress are welcome. We welcome participants from all areas and all levels, but due to space restrictions in the venue, the Kanazawa Noh Museum, we kindly ask to contact Norbert Preining (see below) beforehand.


The workshop takes place at Kanazawa Noh Museum, which is located in the famous sightseeing spot of Kanazawa, including Kenroku-en (Six Attributes Garden), Kanazawa Castle, 21st Century Museum of Contemporary Art, etc... See Kanazawa Tourist Information Guide for more places (in particular, home → tour guide → 01).

Kanazawa Noh Museum
1-2-25 Kosaka, Kanazawa, Ishikawa, Japan


February 8

10:00-11:00 Extraction of Verified Algorithms in Exact Real Arithmetic (slides)
Ulrich Berger

According to the Curry-Howard correspondence a constructive proof contains an algorithm solving the computational problem expressed by the formula proven. Program extraction form proofs exploits this correspondence for the automatic generation of verified programs. Usually, this is applied to combinatorial problems involving discrete data. We show that it is also possible to extract programs operating on non-discrete data such as real numbers and continuous real functions.

– Break –
11:20-12:00 Program Extraction from Constructive and Classical Proofs: Higman's Lemma
Monika Seisenberger

Higman's Lemma is a theorem with a well-known classical proof using the so-called Minimal-Bad-Sequence Argument. Whilst the proof is short and elegant, its computational content is less obvious. We use Higman's Lemma as an example to discuss program extraction from constructive and classical proofs, and report from our experiences with its formalization in the Interactive Theorem Prover Minlog.

– Lunch Break –
13:50-14:30 Comparing Implicit Characterization by Program Transformations (slides)
Guillaume Bonfante

In the past few years, a plenty of characterizations of complexity classes have been proposed, especially PTIME and PSPACE by means of restrictions of rewriting theories. However, it is hard to compare them. Usually, to illustrate the strength of a theory, the authors propose a remarkable example. We propose to compare theories by closure under transformations.

14:30-15:10 Formalization of Mathematics (slides)
Masahiko Sato

We discuss the possibility of formalizing mathematics from a point of view where mathematics is understood as a human linguistic activity. We will do this by designing a programming language which can be used not only to compute mathematical objects as data but can be also used to prove mathematical propositions which are also mathematical objects. The key idea here is that mathematics changes dynamically by the introduction of new concepts.

– Break –
15:30-16:10 Parallel Dialogue Games and Hypersequents for Intermediate Logics (slides)
Christian Fermüller

In an attempt to provide an interpretation of hypersequent systems for various intermediate logic, we relate them to parallel versions of Lorenzen's dialogue game for intuitionistic logic. Augmenting the basic dialogue game by different forms of synchronization mechanisms is shown to correspond to different external structural rules. A prominent example of such a rule is Avron's communication rule that turns a hypersequent system for intuitionistic logic into one for Gödel-Dummett logic. Our results can be understood to provide some underpinning, but also certain qualifications, to the claim advanced by Avron and Baaz that Gödel-Dummett logic relates to parallel programs in a similar way as intuitionistic logic relates to sequential programs. (Note: The talk is based on a paper that appeared already in 2003, but has recently attracted attention by experts in dialogical logic.)

16:10-16:50 Rewriting Techniques in Complexity Analysis (slides)
Nao Hirokawa

Term rewriting is a simple and powerful computational model which underlies theorem proving and functional programs. In this talk we discuss about techniques for estimating (polynomial) time complexities of functions defined by rewrite systems.

– Short Break –
17:00-17:40 Satsifiability in Gödel Logics (slides)
Norbert Preining

The family of Gödel logics is a prominent example of many-valued logics. It is a family of finite- and infinite-valued logics where the sets of truth values are closed subsets of [0, 1] containing 0 and 1. Recent result clarify the status of the satisfiability problem for (full) monadic fragment depending on the topological type of the truth value set. In addition we discuss a first-order fragment of certain Gödel logics extended with Delta that is powerful enough to formalize important properties of fuzzy rule-based systems. For this fragment we show that the satisfiability problem is NP-complete for all truth value sets, even in presence of an additional involutive negation. In contrast with the one-variable case, in the considered fragment only two infinite-valued Gödel logics extended with Delta differ w.r.t. satisfiability. They are determined by a simple topological condition on their respective sets of truth values. Only one of these logics enjoys the final model property.

17:40 – End of First Day –
19:00- – Banquet –

February 9

10:00-11:00 The Finite Embeddability Property for Algebras of Logic (slides)
Constantine Tsinakis

A class of algebras K is said to have the finite embeddability property (FEP) if every finite subalgebra of a member of K can be embedded into a finite member of K. The FEP has strong consequences. For example, it implies the residual finiteness of any finitely presented algebra in a variety, as well as the solvability of the word problem for this variety. The objective of this talk is to provide an overview of the FEP in the realm of universal algebra, and clarify the key role of join-extensions in the establishment of the FEP for important varieties of logic.

– Break –
11:20-12:00 Maximal Completion
Dominik Klein

Completion procedures compute a complete (terminating and confluent) term rewrite system for a given equational system. This talk presents a very simple and efficient completion procedure, which is based on MaxSAT-solving. Experiments show that the procedure is comparable to recent powerful completion tools.

– Lunch Break –
13:00-14:30– Guided Tour of Noh Museum –
14:30-15:10 Epsilon-calculus for Non-classical Logics
Matthias Baaz

In this lecture we discuss range and limitations of the validity of the first and second epsilon theorems for non-classical logics.

15:10-15:40 Power and Limits of Analytic Calculi: Towards a Systematic Proof Theory for Nonclassical Logics
Agata Ciabattoni
– Break –
16:10-16:50 Church => Scott = Ptime: An Application of Resource Sensitive Realizability (slides)
Kazushige Terui

We introduce a variant of linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. The Church encodings of binary words are typed by a standard non-linear type `Church,' while the Scott encodings (purely linear representations of words) are by a linear type `Scott.' We then give a characterization of polynomial time functions, which is derived from (Leivant and Marion 93): a function is computable in polynomial time if and only if it can be represented by a term of type Church => Scott. To prove soundness, we employ a resource sensitive realizability technique developed by Hofmann and Dal Lago. This is a joint work with Alois Brunel.

16:50 – End of Workshop –

Social Events

February 8

We plan to have a banquet at 7 pm.

February 9

A guided tour of the Noh Museum is planned at 1 pm.


Organising Committee

Research Center for Integrated Science (RCIS)

Research Center for Software Verification (jrcSV)

JAIST logoJAIST mark