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
--------------------------------------------------------------------------------