Deadline: MARCH 8TH 1996 FINAL Call for Contributions 3rd Workshop on Logic, Language, Information and Computation (WoLLIC'96) May 8-10, 1996 Salvador (Bahia), Brazil The `3rd Workshop on Logic, Language, Information and Computation' (WoLLIC'96) will be held in Salvador, Bahia (Brazil), from the 8th to the 10th May 1996. Contributions are invited in the form of two-page (600 words) abstracts in all areas related to logic, language, information and computation, including: pure logical systems, proof theory, model theory, type theory, category theory, constructive mathematics, lambda and combinatorial calculi, program logic and program semantics, nonclassical logics, nonmonotonic logic, logic and language, discourse representation, logic and artificial intelligence, automated deduction, foundations of logic programming, logic and computation, and logic engineering. There will be a number of guest speakers, including: Andreas Blass (Ann Arbor), Nachum Dershowitz (Urbana-Champaign), J. Michael Dunn (Indiana), Peter G"ardenfors (Lund), Jeroen Groenendijk (Amsterdam), Wilfrid Hodges (London), Roger Maddux (Ames, Iowa), Andrew Pitts (Cambridge), Amir Pnueli (Rehovot), Michael Smyth (London). WoLLIC'96 is part of a larger biennial event in computer science being held in the campus of the Federal University of Bahia from the 6th to the 10th of May 1996: the `6th SEMINFO' (6th Informatics Week). The 6th SEMINFO will involve parallel sessions, tutorials, mini-courses, as well as the XI Brazilian Conference on Mathematical Logic (EBL'96), and a Workshop on Distributed Systems (WoSiD'96). The 3rd WoLLIC'96 is under the official auspices of the Interest Group in Pure and Applied Logics (IGPL) and The European Association for Logic, Language and Information (FoLLI). Abstracts will be published in the Journal of the IGPL (ISSN 0945-9103) (up to now produced and distributed by Imperial College, London, and Max-Planck-Institut, Saarbruecken, but soon to be distributed by Oxford University Press) as part of the meeting report. Selected contributed papers will be invited for submission (in full version) to a special issue of the Journal (http://www.mpi-sb.mpg.de/igpl/Journal). The 3rd WoLLIC'96 is also sponsored by the Association for Symbolic Logic (ASL). Submission: Two-page abstracts, preferably by e-mail to *** wollic96@di.ufpe.br *** must be RECEIVED by MARCH 8th, 1996 by the Chair of the Organising Committee. Authors will be notified of acceptance by April 8th, 1996. The location: Salvador, Capital of the Bahia state, the first European settlement of Portuguese America and the first Capital of Brazil, is where all the most important colonial buildings were constructed: churches, convents, palaces, forts and many other monuments. Part of the city historical center has been safekept by UNESCO since 1985. Five hundred years of blending Native American, Portuguese, and African influences have left a rich culture to its people, whichcan be felt on its music, food, and mysticism. Salvador is located on the northeastern coast of Brazil and the sun shines year round with the average temperature of 25 degrees Celsius. It is surrounded by palm trees and beaches with warm water. City population is around 2.5 million and life style is quite relaxed. Programme Committee: W. A. Carnielli (UNICAMP, Campinas), M. Costa (EMBRAPA, Brasilia), V. de Paiva (Cambridge Univ., UK), R. de Queiroz (UFPE, Recife), A. Haeberer (PUC, Rio), T. Pequeno (UFC, Fortaleza), L. C. Pereira (PUC, Rio), K. Segerberg (Uppsala Univ., Sweden), A. M. Sette (UNICAMP, Campinas), P. Veloso (PUC, Rio). Organising Committee: H. Benatti (UFPE), L. S. Baptista (UFPE), A. Duran (UFBA), T. Monteiro (UFPE), A. G. de Oliveira (UFBA), N. Riccio (UFBA). For further information, contact the Chair of Organising Committee: R. de Queiroz, Departamento de Informatica, Universidade Federal de Pernambuco (UFPE) em Recife, Caixa Postal 7851, Recife, PE 50732-970, Brazil, e-mail: ruy@di.ufpe.br, tel.: +55 81 271 8430, fax: +55 81 271 8438. (Co-Chair: T. Pequeno, LIA, UFC, tarcisio@lia.ufc.br, fax +55 85 288 9845) Web homepage: http://www.di.ufpe.br/simposios/wollic.html -------------------------------------------------------------------------------- 3rd Workshop on Logic, Language, Information and Computation (WoLLIC'96) May 8-10, 1996 Salvador (Bahia), Brazil TITLE AND ABSTRACT OF INVITED TALKS -------------------------------------------------------------------------------- Some Semantical Aspects of Linear Logic Andreas Blass I plan to discuss some of the semantics that have been proposed for Girard's linear logic, including different forms of game semantics, de Paiva's Dialectica-like semantics, and perhaps others. I shall describe how these semantics are related to each other, to the intuitions that underlie linear logic, and to some other parts of mathematics. -------------------------------------------------------------------------------- Trees, Ordinals, and Termination Nachum Dershowitz Trees are a natural representation for countable ordinals. We describe natural well-founded orderings of finite binary trees, finite ordered (plane-planted) trees, rational binary trees (finite or infinite binary trees with only finitely many different subtrees), and "supertrees" (trees whose nodes may themselves be supertrees). We relate these orderings to existing ordinal notations, and illustrate their use in various colorful termination problems. -------------------------------------------------------------------------------- Proof Theory and Semantics for Structurally Free Logics J. Michael Dunn This work is joint with R. K. Meyer. The idea is to provide a semantics and proof theory for combinatory logic, extended by a "residual" (implication). The semantics is a variation on the ternary relational (Meyer-Routley) semantics for relevance logic, as extended by Meyer-Routley, and more recently others for the (fusion-implication) fragment of the relevance logic B+ (closely related to the non-associative Lambek calculus). The proof-theory extends some semi-published work of Meyer in the 1970's (following a suggestion of Belnap), wherein Gentzen's structural rules for the intuitionistic implication calculus were replacewith explicit introduction of a combinator licensing the combinatorial manipulations. This is extended so as to make combinators "first-class objects," and a cut theorem can still be proven. This is called "structurally free logic" in analogy with "logic freed of existential presppositions." In this original "free logic," existence presuppositions are made explicit, just as in "combinatorially free logic" combinatorial moves are made explicit by adding the combinators that license them as explicit premisses in the antecedent of the sequent. This allows various logics to be translated into the combinatorially free logic. It also expands the meaning of "substructural logics" beyond the usual ones obtained by considering various subsets of Gentzen's structural rules (plus say associativity). There will also be results about adding other connectives (conjunction and disjunction), with or without distribution. -------------------------------------------------------------------------------- Three Levels of Knowledge Representation Peter G"ardenfors Within logic, AI and early cognitive science, almost all research concerning knowledge representation has been based on symbolic (propositional) models. In the 80's connectionist models became popular as an alternative way of modelling knowledge. I propose that also a third type of knowledge representation based on conceptual models should be studied. In particular, I will discuss conceptual models based on geometrical and topological notions and show their relevance for concept revision and for non-monotonic aspects of concepts. I will argue that conceptual models of knowledge can be seen as a bridge between symbolic and connectionist representations. The three kinds of knowledge representation models should thus not be seen as competitors, but rather as complementary models suitable for different modelling tasks. -------------------------------------------------------------------------------- Update Semantics Meets Discourse Jeroen Groenendijk In update semantics the meaning of a sentence is identified with its potential to change the information state of an agent. In the recursive semantic definition, truth conditions are replaced by update effects. Central notions are not truth and validity, but consistency, support, and coherence. Although update semantics is advertized as addressing itself to the interpretation of discourse, rather than being limited to single sentences, it usually goes no further than interpreting sequences of utterances of a single agent. In the present talk I will study the interpretation of multi-agent discourse. The object language we investigate is the language of modal predicate logic. We concentrate on the role of (epistemic) modalities in discourse, and on anaphoric relations (binding of variables) across utterances of different speakers. The aim is to characterize notions of logical consistency and coherence of multi-agent discourse. The paper reports on joint work with Martin Stokhof and Frank Veltman. -------------------------------------------------------------------------------- TBA Wilfrid Hodges -------------------------------------------------------------------------------- Sequential Algebras Roger Maddux The sequential calculus of von Karger and Hoare ("Sequential Calculus", Inform. Process. Lett. 53(1995), 123-130) is designed for reasoning about sequential phenomena, dynamic or temporal logic, concurrent or reactive systems, and so on. Unlike the classical calculus of relations, it has no operation for forming the converse of a relation. Sequential algebras are defined by von Karger so that sequential calculus turns out to be the equational theory of the class of sequential algebras. A standard example of a sequential algebra is the powerset of a partial ordering (a transitive reflexive relation) with Boolean operations (union, etc.), composition, and two operations that are conjugate to composition. Nonstandard examples arise by relativizing nonrepresentable relation algebras to elements that are transitive and reflexive. The incompleteness and non-finite-axiomatizability of the sequential calculus will be presented through some new constructions of sequential algebras and relation algebras. These algebras improve on previous examples in certain interesting respects and give yet another proof that the classical calculus of relations is not finitely axiomatizable. This is joint work with Peter Jipsen (Cape Town). -------------------------------------------------------------------------------- "Logical" Relations between Syntax and Semantics Andrew Pitts In this talk I will discuss some recent developments in the mathematical foundations of programming language semantics. On the one hand, Freyd's categorical analysis of recursively defined domains has led to simplified techniques for denotational semantics involving such domains. On the other hand, work of Abramsky, Howe and others on co-inductively defined "applicative bisimulations" has provided quite powerful theories of equivalence of functional programs, defined in terms of their operational semantics. I will tie together some of these developments by describing a certain "logical relation" between the syntax and semantics of lambda calculus which can be used to derive extensionality and continuity properties of operationally-defined program equivalences from corresponding properties of recursively defined domains. The logical relation itself goes back to Plotkin. What is new is the recognition that the relation has a certain property (a "universal property", in category-theoretic terms) which both characterises it uniquely and permits the operationally-based properties to be derived. -------------------------------------------------------------------------------- Verifying Timed and Hybrid Systems Amir Pnueli The talk presents new computational models for real-time and hybrid systems. For timed systems we propose a model called A Clocked Transition System (CTSS). The CTSS model is a development of our previous Timed Transition model, where some of the changes are inspired by the model of Timed Automata. The new models lead to a simpler style of temporal specification and verification, requiring no extension of the temporal language. We present verification rules for proving safety properties (including time-bounded response properties) of clocked transition systems, and separate rules for proving (time-unbounded) response properties. To justify the need for time-unbounded resopnse rules, we present a characteristic example of a timed system which terminates but no apriori bound on its termination time can be given All rules are associated with verification diagrams. The verification of RESPONSE properties requires adjustments of the proof rules developed for untimed systems, reflecting the fact that progress in the real time systems is ensured by the progress of time and not by fairness. The style of the verification rules is very close to the verification style of untimed systems which allows the (re)use of verification methods and tools, developed for untimed reactive systems, for proving properties of real-time systems. We conclude with the presentation of a branching-time based approach for verifying that an arbitrary given CTSS is Non-Zeno. This is joint work with Y. Kesten and Z. Manna. -------------------------------------------------------------------------------- TBA Michael Smyth --------------------------------------------------------------------------------