View: session overviewtalk overviewside by side with other conferences
08:45  Undecidability of consequence relation in Full Nonassociative Lambek Calculus SPEAKER: Karel Chvalovský ABSTRACT. We prove that the consequence relation in the Full Nonassociative Lambek Calculus is undecidable. 
09:15  Canonical formulas for kpotent residuated lattices SPEAKER: Luca Spada ABSTRACT. We present a method, which generalises canonical formulas for intuitionistic logic, to axiomatise all varieties of kpotent residuated lattice. 
09:45  On satisfiability of terms in FLewalgebras SPEAKER: Zuzana Hanikova ABSTRACT. A paper on satisfiability of terms in FLewalgebras. 
08:45  Fivevalued LTL for Runtime Verification SPEAKER: Ming Chai ABSTRACT. we investigate a monitoring approach based on linear temporal logic (LTL) specifications. The fivevalued 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. 
09:15  A method for generalizing finite automata arising from Stonelike dualities SPEAKER: Denisa Diaconescu 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 settheoretical 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 nonclassical 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 Lfortress and hence studying the language accepted by such an object. We investigate the following question: What is the reflection of Lfortresses in the theory of automata? We explicit our method for Godel logic. 
09:45  An application of distancebased approximate reasoning for diagnostic questionnaires in healthcare SPEAKER: unknown ABSTRACT. In this talk we propose a formal degreebased framework for computing scores in medical assessment questionnaires. 
10:45  Combining Intuitionistic and Classical Logic: a proof system and semantics SPEAKER: Dale Miller 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.

11:45  Tutorial 2/2: The more, the less, and the much more: An introduction to Lukasiewicz logic as a logic of vague propositions, and to its applications SPEAKER: Vincenzo Marra ABSTRACT. In the second talk I show through examples how the availability of such an intended semantics, far from being 
14:30  Embeddings into BiFLalgebras and conservativity SPEAKER: unknown 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 dualimplicationfree fragment of the corresponding calculus. The same conservativity result follows for all the axiomatic extensions by the above equations. 
15:00  The lattice of varieties generated by small residuated lattices SPEAKER: Peter Jipsen ABSTRACT. We describe the bottom of the lattice of varieties of residuated lattices and FLalgebras by calculating the HSposet 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, BLalgebras, MValgebras and Gödel algebras. From this data one can deduce some structural properties of residuated lattices. 
15:30  Quasivarieties of MValgebras and structurally complete Lukasiewicz logics SPEAKER: Joan Gispert ABSTRACT. This paper is a contribution to the study of the lattice of all quasivarieties of MValgebras. For every proper subvariety V of MValgebras we investigate the least quasivariety K in V that generates V as a variety. For every least Vquasivariety we obtain a finite set of generators. Finally we apply some of the algebraic results to obtain results in admissibility theory of Lukasiewicz logics. 
14:30  Booleanvalued judgment aggregation SPEAKER: unknown ABSTRACT. [From the abstract's concluding paragraph; FOR THE FULL ABSTRACT, PLEASE SEE THE ATTACHED FILE.] We describe a framework for Booleanvalued 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 orderpreservation 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. 
15:00  Constructing manyvalued logical functions with small influence of their variables SPEAKER: unknown ABSTRACT. The Boolean functions with small influence of their inputs are used in the collective coin flipping algorithms [BenOr, Linial: Collective coin flipping, Randomness and Computation 1989, 91115]. In this contribution we replace the random bit generator with a random generator over a finite set and we show the existence of finitelyvalued Lukasiewicz formulas with small influence of their variables. 
15:30  Coupling games for Lukasiewicz logic SPEAKER: Alex Simpson 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. 
16:30  Foundations and Technology Competitions Award Ceremony 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:
The following three Boards of Jurors were in charge of choosing the winners:
http://fellowship.logic.at/ 
17:30  FLoC Olympic Games Award Ceremony 1 SPEAKER: Floc Olympic Games 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

18:15  FLoC Closing Week 1 SPEAKER: Helmut Veith 
16:30  Densification via polynomial extensions SPEAKER: Rostislav Horcik 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. 
17:00  Introducing an exotic MTLchain SPEAKER: Felix Bou ABSTRACT. It is shown an equation which only involves the lattice operations (meet and join) and the monoidal operation that is valid in BLchains while it fails in some MTLchains. 
17:30  On Pocrims and Hoops SPEAKER: unknown 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. 
16:30  Ordinal foundation for Lukasiewicz semantics SPEAKER: Rossella Marrano ABSTRACT. We investigate the relationship between the standard pointwise truthvalue semantics for Lukasiewicz infinitevalued logic and an orderingbased 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 realvalued Lukasiewicz valuation. We discuss the desirability of these conditions as properties of the relation intuitively interpreted as `being less true'. 
17:00  Advances on elementary equivalence in model theory of fuzzy logics SPEAKER: unknown ABSTRACT. Elementary equivalence is a central notion in classical model theory that allows to classify firstorder structures. It has received several useful characterizations, among others, in terms of systems of backandforth, and has yielded many important results like the general forms of LowenheimSkolem 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. 
17:30  Trakhtenbrot theorem and firstorder axiomatic extensions of MTL SPEAKER: Matteo Bianchi ABSTRACT. In 1950, B.A. Trakhtenbrot showed that the set of firstorder tautologies associated to finite models is not recursively enumerable. In 1999, P. H\'ajek generalized this result to the firstorder versions of \L ukasiewicz, G\"odel and Product logics. In this talk we extend the analysis to the firstorder 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 Lchain $\mathcal{A}$ the set fTAUT$^\mathcal{A}_{\forall}$ (the set of firstorder 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 Lchain $\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. 