Workshop on Logic and Computation

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.

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.

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.

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.

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

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.

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.

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.

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.

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

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.