ABSTRACT. We present a unifying categorical approach, based on Joyal’s completeness theorem, that proves constructive completeness theorems for classical and intuitionistic first order logic, as well as for the coherent fragment. We show that the notion of exploding structure introduced by Veldman in 1976 is adequate for certain fragments of first-order logic, and that Veldman’s modified Kripke semantics arises, as a consequence, as the semantics of a suitable sheaf topos. The proof, as that of Veldman’s, makes essential use of the Fan theorem, since we show that these completeness theorems are in fact equivalent to it. This raises the question of how far one can get in proving completeness constructively but without using the Fan theorem. We prove that the disjunction-free fragment is constructively complete without appealing to it, and also without placing restrictions on the decidability of the theories and the size of the language, while the latter is a fundamental constraint in the general case when working in intuitionistic set theory. Along the way, we show that the completeness of Kripke semantics for the disjunction free fragment is equivalent, over intuitionistic Zermelo-Fraenkel set theory, to the Law of Excluded Middle.

ABSTRACT. We give a short computational proof derived from Henkin's proof of Gödel’s completeness theorem.

ABSTRACT. We define a simply typed lambda calculus with positive recursive types in which we study the less well-known Scott encoding of data types. Scott data types have "case distinction" as a basic feature. We shed a different light on the Scott data types, by viewing the different cases as "continuations". As Scott data types do not have iteration (or recursion) built in, we add as primitives a "call-by-name iterator" and a "call-by-value iterator" with appropriate reduction rules. We show that the calculus is strongly normalizing.

ABSTRACT. We report here on current work towards an effective proof (with explicit bounds) of Podelski and Rybalchenko Termination Theorem [1]. Our long-term project is to obtain a priori-bounds for the termination of computer programs, and compare these with bounds obtained via other intuitionistic proofs of the Termination Theorem.

References

1. Andreas Podelski and Andrey Rybalchenko. Transition invariants. In LICS, pages 32-41, 2004.

ABSTRACT. The third round of the Kurt Gödel Research Prize Fellowships Program, under the title: Connecting Foundations and Technology, aims at supporting young scholars in early stages of their academic careers by offering highest fellowships in history of logic, kindly supported by the John Templeton Foundation. Young scholars being less or exactly 40 years old at the time of the commencement of the Vienna Summer of Logic (July 9, 2014) will be awarded one fellowship award in the amount of EUR 100,000, in each of the following categories:

• Logical Foundations of Mathematics,
• Logical Foundations of Computer Science, and
• Logical Foundations of Artificial Intelligence

The following three Boards of Jurors were in charge of choosing the winners:

• Logical Foundations of Mathematics: Jan Krajíček, Angus Macintyre, and Dana Scott (Chair).
• Logical Foundations of Computer Science: Franz Baader, Johann Makowsky, and Wolfgang Thomas (Chair).
• Logical Foundations of Artificial Intelligence: Luigia Carlucci Aiello, Georg Gottlob (Chair), and Bernhard Nebel.

http://fellowship.logic.at/

ABSTRACT. The aim of the FLoC Olympic Games is to start a tradition in the spirit of the ancient Olympic Games, a Panhellenic sport festival held every four years in the sanctuary of Olympia in Greece, this time in the scientific community of computational logic. Every four years, as part of the Federated Logic Conference, the Games will gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At the Award Ceremonies, the competition organizers will have the opportunity to present their competitions to the public and give away special prizes, the prestigious Kurt Gödel medals, to their successful competitors. This reinforces the main goal of the FLoC Olympic Games, that is, to facilitate the visibility of the competitions associated with the conferences and workshops of the Federated Logic Conference during the Vienna Summer of Logic.

This award ceremony will host the

• 3rd Confluence Competition (CoCo 2014);
• Configurable SAT Solver Challenge (CSSC 2014);
• Ninth Max-SAT Evaluation (Max-SAT 2014);
• QBF Gallery 2014; and
• SAT Competition 2014 (SAT-COMP 2014).

ABSTRACT. Recently, Abel and others have proposed a type system, in which coinductive types are programmed by means of observations. We investigate category theoretical and topological properties of an observational equivalence on terms, which arises naturally in this type system. Moreover, we introduce a proof system, allowing us to verify proofs of observational equivalence.

ABSTRACT. We introduce the explicit counterparts and prove realization theorem for bimodal logics, describing communication of two agents in case when knowledge (belief) of both agents is described by one of the logics $\mathsf{K}$, $\mathsf{T}$ or $\mathsf{K4}$. The agents may interact by either adopting or verifying each others knowledge; interaction can be either one-way or two-ways.