Third 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). 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 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 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, which can 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. -------------------------------------------------------------------------------- TBA Peter G"ardenfors -------------------------------------------------------------------------------- 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 -------------------------------------------------------------------------------- TBA Roger Maddux -------------------------------------------------------------------------------- TBA Andrew Pitts -------------------------------------------------------------------------------- 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 --------------------------------------------------------------------------------