ABSTRACT. We prove that the consequence relation in the Full Non-associative Lambek Calculus is undecidable.

ABSTRACT. We present a method, which generalises canonical formulas for intuitionistic logic, to axiomatise all varieties of k-potent residuated lattice.

ABSTRACT. A paper on satisfiability of terms in FLew-algebras.

ABSTRACT. we investigate a monitoring approach based on linear temporal logic (LTL) specifications. The five-valued logic is introduced for dealing with two kinds of uncertainties in distributed systems. On one hand, the order of causally unrelated executions is not determined when a global clock is not available. On the other hand, in a finite amount of time, the behaviour can be observed only up to a certain moment, and the future behaviour is unknown. We show the feasibility of our approach with a case study in the railway domain.

ABSTRACT. We start our investigation by first providing a dictionary for translating deterministic finite automata (DFA henceforth) in the language of classical propositional logic. The main idea underlying our investigation is to regard each DFA as a finite set-theoretical object, applying the finite slice of Stone duality in order to move from DFA to algebra, and finally using the algebraizability of classical logic to introduce the formal objects which arise by this "translation" and that we call classical fortresses. We show that classical fortresses accept exactly the same languages as finite automata, that is, regular languages.

Classical fortresses, as objects specified in classical propositional logic on a finite number of variables, allow an easy generalization to any non-classical logical setting: given a propositional logical calculus L, one can easily adapt the definition of classical fortress to the frame of L, introducing a notion of L-fortress and hence studying the language accepted by such an object. We investigate the following question: What is the reflection of L-fortresses in the theory of automata? We explicit our method for Godel logic.

ABSTRACT. In this talk we propose a formal degree-based framework for computing scores in medical assessment questionnaires.

ABSTRACT. While Gentzen's sequent calculus provides a framework for developing the proof theory of both classical and intuitionistic logic, it did not provide us with one logic that combines them.  There are, of course, a number of ways to relate classical and intuitionistic logic: for example, intuitionistic logic can be translated into classical logic with the addition of the S4 modality and classical logic can be embedded into intuitionistic logic using negation translations.  Here we consider the problem of building proof systems and semantics for a logic in which classical and intuitionistic connectives mix freely. Our solution, the logic of Polarized Intuitionistic Logic, employs a polarization (red/green) of formulas and two entailment judgments.  We give a Kripke semantics and a sequent calculus for this logic for which soundness and completeness holds.  The sequent calculus proof system mixes elements of Gentzen's LJ proof system and Girard's LC proof system.  This talk is based on joint work with Chuck Liang. 

ABSTRACT. In the second talk I show through examples how the availability of such an intended semantics, far from being
an ornamental addition to the literature, is in fact a sine qua non to deploy Lukasiewicz logic in applications of genuine
importance. In closing, if time allows, I revisit H\’ajek’s Programme in many-valued logic in light of our discussion of
Lukasiewicz logic.

ABSTRACT. We prove that every FL+ algebra can be embedded into a BiFL algebra and also provide equations that are preserved under this embedding. We obtain as corollary that the logic BiFL, which is the multiple conclusion version of Full Lambek calculus, is conservative over the logic defined by the dual-implication-free fragment of the corresponding calculus. The same conservativity result follows for all the axiomatic extensions by the above equations.

ABSTRACT. We describe the bottom of the lattice of varieties of residuated lattices and FL-algebras by calculating the HS-poset of subdirectly irreducible residuated lattices up to size 5. Diagrams of parts of this poset are displayed, with the algebras grouped by well known subvarieties that contain them, such as commutative, integral, distributive and/or representable residuated lattices, BL-algebras, MV-algebras and Gödel algebras. From this data one can deduce some structural properties of residuated lattices.

ABSTRACT. This paper is a contribution to the study of the lattice of all quasivarieties of MV-algebras. For every proper subvariety V of MV-algebras we investigate the least quasivariety K in V that generates V as a variety. For every least V-quasivariety we obtain a finite set of generators. Finally we apply some of the algebraic results to obtain results in admissibility theory of Lukasiewicz logics.

ABSTRACT. [From the abstract's concluding paragraph; FOR THE FULL ABSTRACT, PLEASE SEE THE ATTACHED FILE.]

We describe a framework for Boolean-valued judgment aggregation. While the major body of the literature on judgment aggregation draws attention to inconsistencies between properties of the agenda and properties of the aggregation rule, the simple (im)possibility results in this paper highlight the role of the set of truth values and its algebraic structure. In particular, it is shown that central properties of aggregation rules can be formulated as homomorphy or order-preservation conditions on the mapping between the powerset algebra over the set of individuals and the algebra of truth values. This is further evidence that the problems in aggregation theory are driven by information loss, which in our framework is given by a coarsening of the algebra of truth values.

ABSTRACT. The Boolean functions with small influence of their inputs are used in the collective coin flipping algorithms [Ben-Or, Linial: Collective coin flipping, Randomness and Computation 1989, 91-115]. In this contribution we replace the random bit generator with a random generator over a finite set and we show the existence of finitely-valued Lukasiewicz formulas with small influence of their variables.

ABSTRACT. We propose a new game interpretation for Lukasiewicz logic. The game is played between two players, Maximizer and Minimizer, who respectively try to maximize and minimize the probability that the property expressed by a formula holds. The mechanism used to achieve this is that players construct couplings of probability measures.

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. Inspired by the proof of standard completeness for Uninorm Logic via residuated frames we present a proof that is completely algebraic and resembles standard constructions of ring extensions from classical algebra.

ABSTRACT. It is shown an equation which only involves the lattice operations (meet and join) and the monoidal operation that is valid in BL-chains while it fails in some MTL-chains.

ABSTRACT. This extended abstract presents recent work on the algebraic structures known as pocrims and hoops. We outline a new method for verifying identities over hoops and give examples of its use. Of particular interest are the identities which show that the double negation mapping in a hoop is a hoop endomorphism. We undertake an algebraic analysis of the double negation translations of Kolmogorov, Gentzen and Glivenko viewed as variants on the standard semantics for intutionistic affine logic with respect to a given class of bounded pocrims. We give a semantic version of Troelstra's requirements for a correct double negation translation. We show that all three translations are correct for the class of bounded hoops and that the Kolmogorov translation is correct for the class of all pocrims. We exhibit classes of pocrims for which the Gentzen translation is correct but the Glivenko translation is not and vice versa.

ABSTRACT. We investigate the relationship between the standard point-wise truth-value semantics for Lukasiewicz infinite-valued logic and an ordering-based semantics consisting in pairwise evaluations. The key step is to lay down sufficient conditions for a binary relation over the set of sentences to represent a real-valued Lukasiewicz valuation. We discuss the desirability of these conditions as properties of the relation intuitively interpreted as `being less true'.

ABSTRACT. Elementary equivalence is a central notion in classical model theory that allows to classify first-order structures. It has received several useful characterizations, among others, in terms of systems of back-and-forth, and has yielded many important results like the general forms of Lowenheim-Skolem theorems. In the context of fuzzy predicate logics, the notion of elementarily equivalent structures was defined Hájek and Cintula. They presented a characterization of conservative extension theories using the elementary equivalence relation. A related approach is the one presented by Novák, Perfilieva and Mockor where models can be elementary equivalent in a degree d. A few recent papers have contributed to the development of model theory of predicate fuzzy logics. However, the understanding of the central notion of elementary equivalence is still far from its counterpart in classical model theory. The present contribution intends to provide some advances towards this goal.

ABSTRACT. In 1950, B.A. Trakhtenbrot showed that the set of first-order tautologies associated to finite models is not recursively enumerable. In 1999, P. H\'ajek generalized this result to the first-order versions of \L ukasiewicz, G\"odel and Product logics. In this talk we extend the analysis to the first-order axiomatic extensions of MTL. Our main result is the following: let L be an axiomatic extension L of MTL whose corresponding variety is generated by a chain. Then if L is an extension of BL or an extension of SMTL or an extension of WNM, for every generic L-chain $\mathcal{A}$ the set fTAUT$^\mathcal{A}_{\forall}$ (the set of first-order tautologies associated to the finite $\mathcal{A}$-models) is $\Pi_1$-complete. More in general, for every axiomatic extension L of MTL there is no L-chain $\mathcal{A}$ such that L$\forall$ is complete w.r.t. the class of finite $\mathcal{A}$-models. We have negative results also if we expand the language with the $\Delta$ operator.