[Prev][Next][Index][Thread]
MFCS'93 information booklet, plain text.
[Since it is clearly relevant, I am distributing this conference
announcement to types. General conference announcements should go to
the Theory-A list. -- Philip Wadler, moderator, Types Forum.]
The following contains the MFCS'93 information booklet
Contents:
l. 19 General information
l. 553 Registration form
l. 610 The abstracts of the talks
********************************************************************
Call for Participation
and Preliminary Programme
MFCS'93
18th International Symposium
on
Mathematical Foundations of Computer Science
Gdansk, Poland
30 August -- 3 September, 1993
ABOUT THE SYMPOSIUM
The MFCS symposia have been organized in Poland and Czecho-Slovakia
since 1972. Their purpose is to encourage high-quality research in
all branches of Theoretical Computer Science, in particular
concurrency, lambda calculus, semantics and logics of programs,
specification, complexity, algorithms, automata theory.
This coming MFCS'93 is organized by the Institute of Computer Science
of the Polish Academy of Sciences.
SCIENTIFIC PROGRAMME
Basing on comments from more than 230 referees the Programme
Committee has selected 56 papers out of 133 submissions. Twelve
invited speakers complete the Symposium's scientific programme.
All contributions and the invited lectures will be printed in
conference Proceedings. The Proceedings will be published in the
Springer-Verlag LNCS series and will be available during the
conference.
Invited Lecturers
K. R. Apt (Amsterdam)
A. Arnold (Bordeaux)
R. M. Burstall (Edinburgh)
V. Diekert (Stuttgart)
M. Hennessy (Brighton)
F. Honsell (Udine)
R. Milner (Edinburgh)
A. Pitts (Cambridge)
V. Pratt (Stanford)
G. Rozenberg (Leiden)
A. Salomaa (Turku)
P. Wadler (Glasgow)
Programme Committee
J. Adamek (Prague)
M. Bednarczyk (Gdansk)
J. A. Bergstra (Amsterdam)
A. M. Borzyszkowski (Gdansk)
B. Courcelle (Bordeaux)
H.-D. Ehrich (Braunschweig)
I. Havel (Prague)
G. Huet (Paris)
N. Jones (Copenhagen)
E. Moggi (Genova)
V. Nepomniaschy (Novosibirsk)
E.-R. Olderog (Oldenburg)
F. Orejas (Barcelona)
A. Poigne (St.,Augustin)
I. Sain (Budapest)
D. Schmidt (Manhattan, Kansas)
S. Sokolowski (Gdansk), chair
M. Wirsing (Munich)
CONFERENCE OFFICE
Please address forms and inquiries to the organizers of the
conference
MFCS'93
Institute of Computer Science
Polish Academy of Sciences
Jaskowa Dolina 31
80-252 Gdansk, Poland
Phone: (+48)(58) 419015 ext. 24,26
Phone: (+48)(58) 419034 ext. 24,26
Fax: (+48)(58) 416912
E-mail: ssokolow@plearn.bitnet
LIST of PRESENTATIONS
Sessions A-n and B-n run in parallel.
MONDAY 30 August, morning
Invited Talk 9.50--10.40
Vaughan Pratt
The second calculus of binary relations
Session A-1 11.10--12.25
Uffe Engberg and Glynn Winskel
Completeness results for linear logic on Petri nets
A. Fantechi, S. Gnesi, and V. Perticaroli
An expressive logic for basic process algebra
Regimantas Pliuskevicius
On saturated calculi for a linear temporal logic
Session B-1 11.10--12.25
Daniele Beauquier and Andreas Podelski
Rabin tree automata and finite monoids
Karel Culik II and Jarkko Kari
Image compression using weighted finite automata
Petr Jancar, Frantisek Mraz, and Martin Platek
A taxonomy of forgetting automata
MONDAY 30 August, afternoon
Invited Talk 14.30--15.20
Phil Wadler
A taste of linear logic
Session A-2 15.30--16.20
Marcin Benke
Efficient type reconstruction in the presence of inheritance
Jian Chen and John Staples
Defining soft sortedness by abstract interpretation
Session B-2 15.30--16.20
Oscar H. Ibarra and Nicholas Tran
On the communication complexity of parallel computation
Juraj Hromkovic, Jarkko Kari, and Lila Kari
Some hierarchies for the communication complexity measures of
cooperating grammar systems
TUESDAY 31 August, morning
Invited Talks 9.00--10.40
Andre Arnold
Equivalences and preorders on transition systems
Matthew Hennessy
Symbolic bisimulations
Session A-3 11.10--12.25
Ilaria Castellani
Observing distribution in processes
David Murphy
Observing located concurrency
Astrid Kiehn
Proof systems for cause based equivalences
Session B-3 11.10--12.25
Hans L. Bodlaender and Klaus Jansen
On the complexity of scheduling incompatible jobs with unit-times
Shiva Chaudhuri, Torben Hagerup, and Rajeev Raman
Approximate and exact deterministic parallel selection
G. S. Frandsen, P. B. Miltersen, and S. Skyum
The complexity of finding replicas using equality tests
TUESDAY 31 August, afternoon
Invited Talk 14.30--15.20
Krzysztof R. Apt
On the unification free Prolog programs
Session A-4 15.30--16.20
Ralf Treinen
Feature constraints with first-class features
Jilei Yin and Hong Zhu
Learning decision lists from noisy examples
Session B-4 15.30--16.20
Z. B. Diskin and I. D. Beylin
Lambda substitution algebras
Don Pigozzi and Antonino Salibra
A representation theorem for lambda abstraction algebras
Session A-5 16.50--17.40
Christophe Cerin and Antoine Petit
Speedup of recognizable trace languages
Peter Ruzicka and Juraj Waczulik
On time-space trade-offs in dynamic graph pebbling
Session B-5 16.50--17.40
Marcello Bonsangue and Joost N. Kok
Isomorphism between predicate and state transformers
Hermann Puhlmann
The snack powerdomain for database semantics
WEDNESDAY 1 September, morning
Invited Talks 9.00--10.40
Grzegorz Rozenberg
An introduction to dynamic labeled 2-structures
Robin Milner
Concrete action structures
THURSDAY 2 September, morning
Invited Talks 9.00--10.40
Volker Diekert
Complex and complex-like traces
Arto Salomaa
Post correspondence problem: Primitivity and interrelations with
complexity classes
Session A-6 11.10--12.25
V. Arvind, J. Kobler, and M. Mundhenk
Hausdorff reduction to sparse sets and to sets of high information
content
Liming Cai and Jianer Chen
On the amount of nondeterminism and the power of verifying
Bruno Martin
A uniform universal CREW PRAM
Session B-6 11.10--12.25
Egidio Astesiano, Gianna Reggio, and Elena Zucca
Stores as homomorphisms and their transformations
J. W. de Bakker, F. van Breugel, and A. de Bruin
Comparative semantics for linear arrays of communicating processes, a
study on the UNIX fork and pipe commands
Werner Stephan and Andreas Wolpers
A calculus for higher order procedures with global variables
THURSDAY 2 September, afternoon
Invited Talk 14.30--15.20
Rod Burstall
Deliverables: a categorical approach to program development
in type theory
Session A-7 15.30--16.20
Bernhard Reus and Thomas Streicher
Verifying properties of module construction in type theory
F. Parisi-Presicce and S. Veglioni
Heterogeneous unified algebras
Session B-7 15.30--16.20
Bruno Durand
Global properties of 2D cellular automata: Some complexity results
Jean Neraud
New algorithms for detecting morphic images of a word
Session A-8 16.50--17.40
Maura Cerioli and Jose Meseguer
May I borrow your logic?
Nicolas Zabel
Analytic tableaux for finite and infinite Post logics
Session B-8 16.50--17.40
Jean Berstel and Patrice Seebold
A characterization of Sturmian morphisms
Philippe Narbel
The boundary of substitution systems
FRIDAY 3 September, morning
Invited Talks 9.00--10.40
Andrew M. Pitts
Observable properties of higher order functions that dynamically
create local names, or: What's new?
Furio Honsell
Some results on the full abstraction problem for restricted lambda
calculi
Session A-9 11.10--12.25
David Stevens
Variable substitution with iconic combinators
Roberto M. Amadio
On the adequacy of PER models
Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro Ugo and Adolfo Piperno
Filter models for a parallel and non deterministic lambda-calculus
Session B-9 11.10--12.25
Liang Chen
A model for real-time process algebras
David Scholefield, Hussein Zedan, and He Jifeng
Real-time refinement: Semantics and application
Bernhard Steffen and Carsten Weise
Deciding testing equivalence for real-time processes with dense time
FRIDAY 3 September, afternoon
Session A-10 14.30--16.10
Laurent Alonso and Rene Schott
On the tree inclusion problem
Louis Ibarra and Dana Richards
Efficient parallel graph algorithms based on open ear decomposition
Egon Wanke
Paths and cycles in finite periodic graphs
Dorothea Wagner and Frank Wagner
Between min cut and graph bisection
Session B-10 14.30--16.10
R. J. van Glabbeek
A complete axiomatization for branching bisimulation congruence of
finite-state behaviours
Pawel Paczkowski
Ignoring nonessential interleavings in assertional reasoning on
concurrent programs
He Jifeng
Hybrid parallel programming and implementation of synchronised
communication
Vladimiro Sassone, Mogens Nielsen, and Glynn Winskel
Deterministic behavioural models for concurrency
Session A-11 16.50--17.40
Pietro di Gianantonio
Real number computability and domain theory.
Michel Parigot and Paul Roziere
Constant time reductions in lambda-calculus
Session B-11 16.50--17.40
J. F. Costa, A. Sernadas, and C. Sernadas
Data encapsulation and modularity: Three views of inheritance
E. de Haas and P. van Emde Boas
Object oriented application flow graphs and their semantics
TRAVEL INFORMATION
Borders and customs
A valid passport is required from all foreign guests. The citizens
of most European states and of the USA need neither entry visas nor
invitations. The citizens of some countries (eg. Canada, Spain,
Portugal, Greece) would need an entry visa. The citizens of some
other countries (Russia, Byelorussia, Ukraine) would need a formal
invitation from the organizers of MFCS'93. The holders of
Lithuanian, Latvian or Estonian passports (not the old Soviet ones!)
need neither visa nor invitation.
As the regulations concerning visas keep changing, please find out in
a Polish consulate in your country. Take into account that
processing your visa application can take a few weeks.
Foreign currencies are easily convertible in Poland in both
directions. Currently, 1 US $ is worth approximately 17000 Polish
Zlotys but this may change. It is advisable to declare money at the
border if you bring them in large quantities (eg. 2000 US$) to be
allowed to take them back legally.
Gdansk-Sobieszewo -- the conference site
The city of Gdansk is situated in the North of Poland in the mouth of
Vistula river, 330 km to the North-North-West from Warsaw, the
capital of Poland. Gdansk is a thousand year old city well known in
both old and recent history. Amber was traded here in Roman Age.
Later, for hundreds of years Gdansk belonged to Hanza and flourished
on trade with Poland while maintaining its semi-sovereignty. The
city was shaped by the Germans, Flemish and Danes, even by the
English and Scottish. Its historical centre is famous for its
brilliant architecture.
The Island of Sobieszewo, a major island in the delta of Vistula
river, used to be a holiday resort for Gdansk citizens. A lake on
the island is regarded as a "birds paradise".
MFCS'93 is organized in the Baltic Conference Center "ORLE",
Lazurowa 8, 80-680 Gdansk-Sobieszewo. The distance from the
conference site to the center of Gdansk is 18 km, while the distance
to the white sandy beaches of the Gdansk Bay is 150 m.
Getting there by train
There are convenient railway connections to Gdansk from Warsaw,
Prague, Berlin (via the nearby Gdynia) and from other cities.
Convenient express or intercity trains leave the Warsaw Central
station (Warszawa Centralna) for Gdansk Main (Gdansk Glowny) at
15.57, 16.57 and 17.57. The journey takes three and a half hours and
costs appr. 300000 zl ($18) in first class carriages.
The MFCS participants arriving at Gdansk Main on Sunday, the 29th
August, by any of the three trains mentioned above will be awaited at
the station and put on a special conference bus for Sobieszewo. We
will extend this option to other trains provided there is enough
interest, so please, fill in the respective information into the
registration form. There will also be a special transportation from
Sobieszewo to Gdansk Main on Saturday, the 4th September.
On Sundays, buses `112' and `186' depart from their stop at the
Gdansk Main railway station for Sobieszewo every 30 minutes on
average, until 22.26.
Taxi fare from the railway station to the conference site is about
250000zl ($15). To avoid overpaying, please negotiate the price with
the taxi driver before getting into the cab.
Getting there by air
Intercontinental and most international flights to Poland arrive at
Warsaw, 330 km from Gdansk.
Domestic (from Warsaw) and some international flights (eg: Hamburg --
daily, London -- on Saturdays and Mondays) arrive at
Gdansk-Rebiechowo Airport. If there is enough interest, the special
Symposium's bus transportation will be extended to the airport.
Buses `110' and `L' depart from the airport to the Gdansk-Wrzeszcz
railway station. The ride takes 20 minutes and costs 6000 zl
($0.35). From there you can take a local train or tramway to Gdansk
Main (Gdansk Glowny) railway station.
Taxi fare from the Airport to the conference site is about 400000 zl
($24).
Getting there by car
If you are coming from Warsaw by road no. 7 (E77), turn right in the
village of Przejazdowo, 8 km before the center of Gdansk, continue
over a pontoon bridge to Sobieszewo and further on, some 3 km through
forest. There, you will come across MFCS posters.
If you are coming from Germany, we suggest the northern route no. 6
(E28) Berlin-Szczecin-Gdynia. Once in the suburb of Gdynia, turn
right into a dual-carriage way towards Gdansk and Lodz. This road
avoids the crowded centres of Gdynia, Sopot and most of Gdansk.
Continue for about 20 km and leave at the junction labelled
Gdansk-Centrum. A 10 km drive will take you to the very centre of
Gdansk; then follow the signs for Warsaw, road no. 7 (E77). After
some 8 km, in Przejazdowo, turn left and proceed as described above.
EXCURSION
On Wednesday, after only two morning talks, a bus excursion is
planned to Malbork and to the old town of Gdansk's, so called Main
Town (Glowne Miasto).
>From the mid-13th until the 15th century, Malbork, or Marienburg, was
the headquarter of the renowned Teutonic Order of monk-knights. The
Order of the Blessed Virgin Mary's Hospital of the German House, as
was their official denomination, arrived there in the beginning of
the 13th century invited by a Mazovian prince to help in fighting
pagan tribes. The Teutonic Knigths took over the land and created
their own state which became Poland's most serious problem for the
next couple of centuries. Their capital, Malbork, was one of the
most inaccessible military strongholds of the time. The castle is
now reconstructed and homes a museum and several expositions --
amber, old armoury etc.
WEATHER
The weather in the beginning of September is usually mild and sunny
but occasional rains are also possible. The temperature ranges from
18 to 24 degrees Centigrade at day, and from 8 to 12 degrees
Centigrade at night. The water temperature in Baltic Sea (the Gulf
of Gdansk) ranges from 15 to 17 degrees Centigrade.
ACCOMMODATION and MEALS
The participants will be lodged in double rooms in the Center. Rooms
will also be available for single occupancy, at an extra cost.
However, the number of rooms in the Center is limited, and only the
early registration will guarantee a single room reservation. Those
registering lately should confirm the availability of rooms in
appropriate category before sending any money.
Meals will be served at the conference site, beginning with supper on
Sunday 29 August, and finishing with breakfast on Saturday 4
September. Please indicate any special dietary requirements on the
registration form.
The registration and information desk will be located at the
conference site. The registration will start on Sunday, August 29 at
16.00.
REGISTRATION and CONFERENCE FEES
The conference fees in US$ are as follows:
until July 14 after July 14
Pro person in a double room 400 450
Single room 450 500
Accompanying person in a double room 280 330
The fee includes:
-- 6 day accommodation with full board (3 meals a day) and
refreshments at coffee breaks from Sunday evening, 29 August, to
Saturday morning, 4 September, at the Baltic Conference Center;
-- All the social events (welcome drink, excursion, conference banquet,
etc.);
-- Conference materials, including the Proceedings of the Symposium.
The accompanying persons' fee includes accommodation, board and
social events but no conference materials.
The participants should transfer the equivalent of the fee in their
local currency to the following Bank account:
Bank Przemyslowo Handlowy w Krakowie
XIV O/Warszawa
Account number: 320007-2408
MFCS'93 <your name>
Institute of Computer Science
Polish Academy of Sciences
Make sure that your payment carries your name and quotes "MFCS'93"
as suggested.
A limited number of grants to partially cover conference expenses
will be available. All the interested are encouraged to apply as
soon as possible.
There is no fee reduction for those who are willing to participate in
a part of the conference only.
In the event of cancellation, the fee will be refunded, except for a
$50 cancellation charge, provided a written request is received by
the conference office by 1st August. Those whose cancellation
request arrives after 1st August will be sent their Proceedings
volume but no money will be returned.
Please complete and mail the form enclosed together with a copy of
the proof of your payment (by regular mail) to the conference
office. The reservation will be confirmed after receiving the proof
of payment.
In case of a late registration (after 1st August) we advise to bring
cash rather than to send money via a bank transfer.
********************************************************************
REGISTRATION AND ACCOMMODATION FORM
Mr/Ms/Dr/Prof ________________________________________
Surname ______________________________________________
Name(s) ______________________________________________
Affiliation __________________________________________
Mailing Address ______________________________________
______________________________________________________
______________________________________________________
Phone(s) ___________________ Fax: ____________________
E-mail: ______________________________________________
RATES in US$. Please indicate the applicable rate by encircling it
on the table, and also writing it in.
until July 14 after July 14
Pro person in a double room 400 450
Single room 450 500
Accompanying person in a double room 280 330
Total fee: ___________________________________________
Sex: _____ female, _____ male
Name of the preferred roommate (if accommodated in a double room):
______________________________________________________
Special dietary requirements (vegetarian, etc.) ______
______________________________________________________
Date of arrival:
_____ by air to Gdansk; approximate time ___________
_____ by train to Gdansk; approximate time _________
_____ by car to Sobieszewo; approximate time _______
Intend to take the conference bus from Gdansk to Sobieszewo:
_____ yes, _____ no.
Date of departure: _________________________________
********************************************************************
ABSTRACTS OF INVITED LECTURES
Krzysztof R. Apt and Sandro Etalle.
On the unification free Prolog programs.
We provide simple conditions which allow us to conclude that in case
of several well-known Prolog programs the unification algorithm can
be replaced by iterated matching. Such a replacement offers a
possibility of improving the efficiency of program's execution.
Andre Arnold and Dicky A.
Equivalences and preorders on transition systems.
Two transition systems are logically equivalent if they satisfy the
same formulas of a given logic. For some of these logics, such as
Hennessy-Milner's logic, there is an algebraic characterization of
this equivalence involving particular homomorphisms of transition
systems. This logical equivalence is associated with a preorder: a
transition system A is less than A' if all formulas satisfied by
A are satisfied by A'. For particular logics, this preorder can
also be algebraically characterized, using homomorphisms and a
specific notion of inclusion of transition systems.
Rod Burstall.
Proofs in type theory.
A number of groups, including one in Edinburgh, are working on proofs
in constructive logic using the elegant propositions as types paradigm. Our
work covers both development of computer checked mathematical theories and
formal development of software.
Volker Diekert.
Complex and complex-like traces.
A. Ehrenfeucht and Grzegorz Rozenberg.
An introduction to dynamic labeled 2-structures.
We introduce the theory of dynamic labeled 2-structures. This theory
forms a framework for investigating (edge-labeled) graphs, where the
relationships between the nodes may change as a result of actions
taking place in the nodes. Thus dynamic labeled 2-structures may be
also seen as models for networks of processes. The lecture presents
basic properties of dynamic labeled 2-structures and it demonstrates
useful links with group theory.
Matthew Hennessy.
Symbolic bisimulations.
Most of the traditional verification methods for process description
languages rely on the fact that the underlying transition systems are
finite branching. If processes are allowed to send and receive
messages or values from an infinite data set then this is rarely the
case. However if we work with "symbolic transition systems" as
opposed to the usual concrete ones then many of the standard methods
can still be applied. This talk will survey recent joint work with H.
Lin and X. Liu on this symbolic approach to message-passing
processes. This will include a theory of symbolic bisimulations,
sound and complete proof systems for mesage-passing process calculi
and a logical characterisation of bisimulation equivalence in terms
of a first-order modal logic.
Furio Honsell and Marina Lenisa.
Some results on the full abstraction problem for restricted lambda
calculi.
I will contrast the denotational accounts of the semantics of
programming languages with other forms of formal description. I will
speak in favour of the former and its infinite constructions both
from a foundational and a technical point of view. I will illustrate
this with some examples. In particular I will discuss some
non-standard limit constructions. One will show that the notion of
non erasing function can be adequately captured mathematically. The
other will be used to show that graspable proofs of operational
properties of lambda calculi can be obtained form the analysis of the
fine structure of models.
Alexandru Mateescu and Arto Salomaa.
Post correspondence problem: Primitivity and interrelations with
complexity classes.
We first introduce the notion of a general primality type, for a
systematic study of "simple", "primitive" or "prime" solutions of
the Post Correspondence Problem. We give an exhaustive
characterization of general primality types. We then introduce
PCP-related complexity classes, for instance, the time complexity
classes PCP-P and PCP-NP. While PCP-NP=NP, we can only show that P is
included in PCP-P.
Robin Milner.
Concrete action structures.
Action structures have been proposed by the author as a general
model, for concurrent computation. An action structure is a monoidal
category with two additions: abstractors, which allow the
parametrization of processes, and reaction, a pre-order upon
morphisms (i.e. actions) which represents their dynamics. They were
designed to understand algebraic process calculi, in particular the
pi-calculus; but the model is wide enough also to supply an
apparently new algebraic treatment of Petri Nets. The lecture will
deal with the narrower class of so-called concrete action structures.
This model allows the pi-calculus (and other process calculi) to be
seen just as the free extension of a certain elementary action
structure by adding certain control primitives. This characterization
offers some hope for a more uniform understanding of process calculi.
Andrew M. Pitts and Ian D. B. Stark.
Observable properties of higher order functions that dynamically
create local names, or: What's new}?}
This talk is concerned with the problem of reasoning about properties
of higher order functions involving state. It is motivated by the
desire to identify what, if any, are the difficulties created purely
by locality of state, independent of other properties such as
side-effects, exceptional termination and non-termination due to
recursion. I consider a simple language (equivalent to a fragment of
Standard ML) of typed, higher order functions that can dynamically
create fresh names. Names are created with local scope, can be tested
for equality and can be passed around by functions, but that is all.
Nevertheless, the observable behaviour of such functions can be very
subtle. I will describe a notion of `applicative equivalence' for
this language incorporating a version of representation independence
for local names. Applicatively equivalent expressions are
observationally equivalent, and the converse is true at first order
types.
Vaughan Pratt.
The second calculus of binary relations.
We first review the Peirce-Schroeder calculus of binary relations,
which equips full linear logic with a nonconstructive noncommutative
interpretation which elegantly and faithfully models the basic
elements of sequential control, but which only weakly models Girard's
axioms. We then reinterpret the same operations over the same domain
to yield a second calculus of binary relations equipping linear logic
with a constructive commutative interpretation which elegantly and
faithfully models the basic elements of concurrent control, and which
models Girard's axioms as soundly and completely as any
Chu-construction model.
Phil Wadler.
A taste of linear logic.
Some of the best things in life are free; and some are not. Truth is
free: having proved a theorem, you may use this proof as many times as
you wish. Food has a cost: having baked a cake, you may eat it only
once. In this sense, traditional logic is about truth, while linear
logic is about food. This talk will describe connections between
traditional logic and the type systems used in functional languages
such as ML and Haskell. It will then go on to describe a type system
based on linear logic, and its application to improving the
expressiveness and performance of functional languages.
ABSTRACTS OF ACCEPTED PAPERS
Laurent Alonso and Rene Schott.
On the tree inclusion problem.
We consider the following problem: Given ordered labeled trees S
and T can S be obtained from T by deleting nodes? Deletion of
the root node u of a subtree with children (T_1,...,T_n) means
replacing the subtree by the trees T_1,...,T_n . For the tree
inclusion problem, there can generally be exponentially many ways to
obtain the included tree. Recently, P. Kilpelainen and H. Manilla
gave an algorithm based on dynamic programming requiring O(|S|.|T|)
time and space in the worst case and also on the average. We give a
new algorithm which improves the previous one on the average and
breaks the |S|.|T| barrier.
Roberto M. Amadio.
On the adequacy of PER models.
We consider a fixed point extension of the second order lambda
calculus equipped with a call by value evaluation mechanism. We
interpret the language in a partial cartesian closed category of
"directed complete" partial equivalence relations (pers) over a
domain theoretic model of a type-free, call-by-value, lambda
calculus. Our main result is that the notions of syntactic and
semantic convergence coincide.
V. Arvind, J. Koebler, and M. Mundhenk.
Hausdorff reduction to sparse sets and to sets of high information
content.
We investigate the complexity of sets that have a rich internal
structure and at the same time are reducible to sets of either low or
very high information content. Measuring the information content of a
set by the space-bounded Kolmogorov complexity of its characteristic
sequence, we show that a set in EXPSPACE is not reducible to a set
having very high information content unless it reduces to a sparse
set.
Egidio Astesiano, Gianna Reggio, and Elena Zucca.
Stores as homomorphisms and their transformations.
We address the problem of giving a clean and uniform mathematical
model for handling user defined data types in imperative languages,
contrary to the ad hoc treatment usual in classical denotational
semantics. The problem is solved by defining the store as a
homomorphic mapping of an algebraic structure of left values
modelling containers into another one of right values modelling
contents. Consequently store transformations can be defined uniformly
on the principle that they are minimal variations of the store
embedding some basic intended effects and compatible with the
homomorphic structure of the store.
Daniele Beauquier and Andreas Podelski.
Rabin tree automata and finite monoids.
We incorporate finite monoids into the theory of Rabin
recognizability of infinite tree languages. We define a free monoid
of infinite trees and associate with each infinite tree language L a
language L^ of infinite words over this monoid. Using this
correspondence we introduce strong} monoid recognizability of
infinite tree languages (strengthening the standard notion for
infinite words) and show that it is equivalent to Rabin
recognizability. We also show that there exists an infinite tree
language L which is not Rabin recognizable, but its associated
language L^ is monoid recognizable (in the standard sense).
Marcin Benke.
Efficient type reconstruction in the presence of inheritance.
The complexity of type reconstruction for simply-typed lambda
calculus with subtype relation resulting from single inheritance (i.e.
being a disjoint union of tree-like posets) is analyzed. As a result
a class of poset including (but not restricted to) trees is defined,
for which the said problem is solvable in polynomial time.
Jean Berstel and Patrice Seebold.
A characterization of Sturmian morphisms.
A morphism is called Sturmian if it preserves all Sturmian (infinite)
words. It is called weakly Sturmian if it preserves at least one
Sturmian word. We prove that a morphism is Sturmian if and only if it
keeps the word ba^2ba^2baba^2bab balanced. As a consequence, weakly
Sturmian morphisms are Sturmian. An application to infinite words
associated to irrational numbers is given.
Hans L. Bodlaender and Klaus Jansen.
On the complexity of scheduling incompatible jobs with
unit-times.
We consider scheduling problems in a multiprocessor system with
incompatibile jobs of unit-time length where two incompatible jobs can
not be processed on the same machine. Given a deadline k' and a
number of k machines, the problem is to find a feasible assignment
of the jobs to the machines. We prove the computational complexity of
this scheduling problem restricted to different graph classes
(cographs, bipartite graphs and interval graphs), arbitary and
constant numbers k and k' .
Marcello Bonsangue and Joost N. Kok.
Isomorphism between predicate and state transformers.
We study the relation between state transformers based on directed
complete partial orders and predicate transformers. Concepts like
"predicate", "liveness", "safety" and "predicate transformers"
are formulated in a topological setting. We treat state transformers
based on the Hoare, Smyth and Plotkin power domains and consider
continuous, monotonic and unrestricted functions. We relate the
transformers by isomorphisms thereby extending and completing earlier
results and giving a complete picture of all the relationships.
Liming Cai and Jianer Chen.
On the amount of nondeterminism and the power of verifying.
The relationship between nondeterminism and other computational
resources is studied based on a special interactive-proof system
model GC(s(n),C) which is a verifier in C that can make an extra
O(s(n)) amount of nondeterminism. We show that for many functions
s(n) and for many complexity classes C, the class GC(s(n),C) has
natural complete languages, and that the classes GC(s(n),\Pi_h^0),
h>=1, characterize precisely the fixed-parameter intractability of
NP-hard optimization problems, where \Pi_h^0 is the class of
languages accepted by log-time k-alternation ATMs.
Ilaria Castellani.
Observing distribution in processes.
The distributed structure of CCS processes can be made explicit by
assigning different locations} to their parallel components. These
locations then become part of what is observed of a process. The
dynamic approach was developed first, in [BCHK91a], [BCHK91b], as it
seemed more convenient for defining notions of location equivalence}
and preorder}. However, it has the drawback of yielding infinite
transition system representations. The static approach, which is
more intuitive but technically more elaborate, was later developed by
L. Aceto [Ace91] for nets of automata}, a subset of CCS where
parallelism is only allowed at the top level. In this approach each
net of automata has a finite representation, and one may derive
notions of equivalence and preorder which coincide with the dynamic
ones. The present work generalizes the static treatment of Aceto to
full CCS. The result is a distributed semantics which yields finite
transition systems for all CCS processes with a regular behaviour.
Christophe Cerin and Antoine Petit.
Speedup of recognizable trace languages.
Traces have been defined by A. Mazurkiewicz in order to modelize
concurrent processes. The decomposition of a trace in foata normal
form gives the "best" parallel execution of a trace. We define
naturally the speedup of a trace as the quotient of its sequential
execution time by its parallel execution time. We generalize this
definition to trace languages and we prove that this speedup can be
computed in a modular way for any recognizable trace language.
Maura Cerioli and Jose Meseguer.
May I borrow your logic?
A general and simple construction is presented that allows borrowing
the components (as well as their associated tools if any) from a logic
that has them in order to enrich another logic missing such features.
The relevant structure is transported using maps involving only some
limited aspect of the two logics in question---for example their
model theory.
Shiva Chaudhuri, Torben Hagerup, and Rajeev Raman.
Approximate and exact deterministic parallel selection.
The selection problem is to find the element of prescribed rank r in
an ordered set. We study approximate and exact selection on
deterministic CRCW PRAMs, where approximate selection asks for any
element whose true rank is close to r. Our main results are
work-optimal approximate selection from n-element sets in
O((loglog n)^4) time and work-optimal exact selection from n-element
sets in O(log n/loglog n) time.
Jian Chen and John Staples.
Defining soft sortedness by abstract interpretation.
To overcome limitations of conventional sorted languages, soft
sorting adds sort signatures to an unsorted language without a priori
restrictions on well-formedness of expressions. Then, the semantics
defines the significance of the sort syntax. This paper shows how
soft sortedness can be defined by abstract interpretations, so as to
characterise semantic properties of softly sorted expressions.
Liang Chen.
A model for real-time process algebras.
We present a general model, Timed Synchronization Trees, for
real-time systems. Timed synchronization trees are extensions of
synchronization trees with time. All constructions are continuous
with respect to a natural CPO. This allows us to interpret a wide
range of real-time process algebras. As an example, we give a
denotational semantics for Timed CCS based on timed synchronization
trees.
J. F. Costa, A. Sernadas, and C. Sernadas.
Data encapsulation and modularity: Three views of
inheritance.
A rich mechanism of inheritance, including both specialization and
abstraction, is essential for supporting the envisaged levels of
software reuse. We adopt the view that an object is a state-machine,
adapting the notion of reactive system. Then, we develop the notion
of object morphism in order to explain the basic relationhips between
objects: is-a and is-part-of.
Karel Culik II and Jarkko Kari.
Image compression using weighted finite automata.
We introduce Weighted Finite Automata (WFA) as a tool to define real
functions, in particular, greyness functions of grey-tone images.
Mathematical properties and the definition power of WFA have been
studied by Culik and Karhumaki. Their generative power is
incomparable with Barnsley's Iterative Function Systems. Here, we
give an automatic encoding algorithm that converts an arbitrary
grey-tone-image (a digitized photograph) into a WFA that can
regenerate it (with or without information loss). The WFA seems to be
the first image definition tool with such a relatively simple
encoding algorithm.
J. W. de Bakker, F. van Breugel, and A. de Bruin.
Comparative semantics for linear arrays of communicating processes, a
study on the UNIX fork and pipe commands.
Operational (O) and denotational (D) semantic models are designed for
a language incorporating a version of the UNIX fork and pipe
commands. Taking a simple while language as starting point, a number
of programming constructs are added which achieve that a program can
generate a dynamically evolving (linear) array of processes connected
by channels. Over these channels sequences of values (`streams') are
transmitted. Both O and D are defined as (unique) fixed point of a
contractive higher ord operator. This allows a smooth proof that O
and D are equivalent. Additional features are the use of hiatons,
and of both syntactic and semantic versions of continuations.
E. de Haas and P. van Emde Boas.
Object oriented application flow graphs and their semantics.
In this paper we present a language called OOAFG and its semantics.
OOAFG intends to express parallelism in the context to object
identity. We believe that the approach to parallelism we take here is
a kind of parallelism that is relatively unexplored which connects
both to the world of Object Oriented Programming, and to the dataflow
paradigm.
Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro and Adolfo Piperno.
Filter models for a parallel and non deterministic
lambda-calculus.
Type assignment systems for the parallel and non deterministic
lambda-calculus are studied together with a denotational semantics
which is initially defined constructing a set semimodel via Curry
types. The type system is then enriched with intersection and union
types, dually reflecting the disjunctive and conjunctive behaviour of
the operators; a filter model is built whose local structure is
compared with a Morris style operational semantics.
Pietro di Gianantonio.
Real number computability and domain theory.
We propose a possible implementation, using lazy functional
programming, of the exact computation on real numbers. Using domain
theory we analyze this kind of computation. An interesting connection
between Scott Topology and the topologies on the real line is stated.
The main original result in this work is the proof that every
computable functional on real numbers is continuous w.r.t. the
compact open topology.
Z. B. Diskin and I. D. Beylin.
Lambda substitution algebras.
In the paper an algebraic metatheory of type-free lambda calculus is
developed. The present version is based on substitution algebras
introduced by Feldman enriched with a countable family of unary
operations of lambda-abstraction and a binary operation of
application. There are proved representation theorems what provides
completeness theorems.
Bruno Durand.
Global properties of 2D cellular automata: Some complexity
results.
In this paper, we prove the co-NP-completeness of the following
decision problem: given a 2-dimensional cellular automaton A, is A
injective when restricted to finite configurations not greater than
its length. In order to prove this result, we introduce two decision
problems concerning respectively Turing Machines and tilings that we
prove NP-complete. We then transform problems concerning tilings into
problems concerning cellular automata.
Uffe Engberg and Glynn Winskel.
Completeness results for linear logic on Petri nets.
Completeness is shown for several versions of Girard's linear logic
with respect to Petri nets as the class of models. The strongest
logic considered is intuitionistic linear logic, with $\otimes$,
$\mathbin{-\mkern-3mu\raise-.21ex\hbox{$\lhook\mkern-3mu \rhook$}}$,
$\vphantom{\oplus}\raise-1.15pt\hbox{\rm\&}$, $\oplus$ and the
exponential ${!}$ ("of course"), and forms of quantification. This
logic is shown sound and complete with respect to atomic nets (these
include nets in which every transition leads to a nonempty multiset
of places). The logic is remarkably expressive, enabling descriptions
of the kinds of properties one might wish to show of nets; in
particular, negative properties, asserting the impossibility of an
assertion, can also be expressed.
A. Fantechi, S. Gnesi, and V. Perticaroli.
An expressive logic for basic process algebra.
In this paper we present a branching time temporal logic for Basic
Process Algebra. This logic is an enrichment of the branching temporal
logic CTL with a branching sequential composition operator, named
chop branching. The logic so obtained is proved to be expressive with
respect to the bisimulation semantics defined on ${\rm
BPA}_{{\textstyle \delta},{\textstyle rec}}}$ terms, and is able to
de scribe context-free properties of systems.
G. S. Frandsen, P. B. Miltersen, and S. Skyum.
The complexity of finding replicas using equality tests.
We prove (for fixed $k$) that at least $\frac{1}{k-1}(^n_2)-O(n)$
equality tests and no more than $\frac{2}k(^n_2)+O(n)$ equality tests
are needed in the worst case to determine whether a given set of $n$
elements contains a subset of $k$ identical elements. The upper bound
is an improvement by a factor $2$ compared to known results. We give
tighter bounds for $k=3$.
Juraj Hromkovic, Jarkko Kari, and Lila Kari.
Some hierarchies for the communication complexity measures of
cooperating grammar systems.
We investigate the descriptional and the computational complexity of
parallel communicating grammar systems (PCGS). A new descriptional
complexity measure---the communication structure of the PCGS---is
introduced and related to the communication complexity (the number of
communications). Several hierarchies resulting from these complexity
measures and some relations between the measures are established. The
results are obtained due to the development of two lower-bound proof
techniques for PCGS.
Louis Ibarra and Dana Richards.
Efficient parallel graph algorithms based on open ear
decomposition.
We present a new technique called "disjoint decreasing ear paths",
which is based on a graph's open ear decomposition. We apply this
technique in CRCW PRAM parallel algorithms for the two vertex
disjoint s-t paths problem and the maximal path problem in planar
graphs. These run in O(log n) time with n+m processors and
O(log^2 n) time with O(n) processors, respectively, where the
graph has n vertices and m edges.
Oscar H. Ibarra and Nicholas Tran.
On the communication complexity of parallel computation.
We argue that the synchronized alternating finite automaton (SAFA) is
a viable model for studying the communication complexity of parallel
computation. This motivates our study of the classes of languages
accepted by SAFA whose messages are bounded in length by a function
m(n). We establish tight lower bounds on m(n) for some types of
SAFA to accept nonregular languages and give a characterization of NP
in terms of SAFA.
Petr Jancar, Frantisek Mraz, and Martin Platek.
A taxonomy of forgetting automata.
Forgetting automata are nondeterministic linear bounded automata
whose rewriting capability is restricted as follows: each cell of the
tape can only be "erased" (rewritten by a special symbol) or
completely "deleted". All classes of languages corresponding to
various combinations of operations are considered and classified
according to the Chomsky hierarchy and (some) other relations among
them are shown.
He Jifeng.
Hybrid parallel programming and implementation of synchronised
communication.
An occam program is usually translated into a machine program
executed in parallel with a set of system processes such as
communication protocal and scheduler, where the target program
appears in a form which cannot be modelled in a purely
communication-based parallel language since concurrent components
share variables. This paper presents a mathematical treatment for a
hybrid language equipped with a parallel construct, whose
sub-processes can communicate with each other via both channels and
shared variables. We show how it can help in the implementation of
concurrency and synchronised communication of occam.
A. Kiehn.
Proof systems for cause based equivalences.
Two proof systems for the congruences of causal bisimulation and
location equivalence of finite CCS are proposed. They generalize the
known axiomatizations for restriction free processes which are based
on the two merge operators of ACP. Since the proof systems only
differ in three equations they provide a simple means of comparison.
Bruno Martin.
A uniform universal CREW PRAM.
The universality of the Parallel Random-Access Machines is usually
defined by simulating universal Turing machines or Boolean networks.
We propose in this paper another definition for the universality of
the Parallel Random-Access Machines based on cellular automata and we
discuss the advantages and drawbacks of this simulation. We prove
that there exists a Concurrent-Read Exclusive-Write Parallel
Random-Access Machine which is capable of simulating any given
cellular automaton in constant time. We then derive to the definition
of complexity classes for the parallel Random-Access Machines and for
the cellular automata.
David Murphy.
Observing located concurrency.
We present a process algebra with an explicit notion of location, and
give three semantics for it. Two of these semantics are operational,
giving a standard interleaving and a wholly distributed model for the
algebra. The third is denotational, and is based on a topology over
the set of locations. This topology allows observers to specify
which locations are to be regarded as distinct. We show that the
denotational semantics is fully abstract with respect to the
interleaving semantics if the topology is indiscrete, and that it
coincides with the fully distributed semantics if it satisfies the
separation axiom T_1.
Philippe Narbel.
The boundary of substitution systems.
The global limit set has been introduced in a preceding work as a
generalization of the way of generating infinite words by
substitution systems, i.e. by iterating a morphism on a finite
alphabet. We prove here that the boundary set (the "adherence
set"), that is the set of the compactification points of a
progressive substitution language is equal to its global limit set
plus a rational set of words. This allows us to exhibit conditions to
conclude that the full boundary is explicitly constructible,
rationally codable and uncountable. The equivalence problem for
boundaries is also shown decidable whenever the iterated morphism is
primitive.
Jean Neraud.
New algorithms for detecting morphic images of a word.
We present efficient algorithms for two subcases of the general
NP-complete problem which consists in matching patterns with
variables:
-- matching an arbitrary one variable regular
expression with constants,
-- matching a two variable pattern.
Pawel Paczkowski.
Ignoring nonessential interleavings in assertional reasoning on
concurrent programs.
In the adopted assertional framework the inductive assertions method
is applied to a labelled transition system representing a program
under verification. A reduced representation of concurrent programs
is considered, where some nonessential interleavings of actions are
ignored. To isolate such interleavings Mazurkiewicz's trace
equivalence is exploited. Decidability of verifying that a given
labelled transition system is a reduced representation of a program
is investigated.
Michel Parigot and Paul Roziere.
Constant time reductions in lambda-calculus.
F. Parisi-Presicce and S. Veglioni.
Heterogeneous unified algebra.
The framework of Unified Algebras, recently developed for the
axiomatic specification of ADT, is modified by introducing again the
notion of sort as a classification mechanism for elements of a type.
While retaining the idea of sorts as values, Heterogeneous Unified
Algebras allow the distinction between certain sorts and the
definition of subsorts by applying operations to them. A
Specification Logic (which can be extended to an Institution using
only injective signature morphisms) is defined, and initial algebra
and free construction are shown to exist.
Don Pigozzi and Antonino Salibra.
A representation theorem for lambda abstraction algebras.
The concept of a lambda abstraction algebra (LAA) is designed to
algebraize the untyped lambda calculus. The equational axioms of
LAA's reflect alpha-conversion and Curry's recursive axiomatization
of substitution in the lambda calculus. Functional LAA's arise from
lambda models, the natural models of the lambda calculus. Questions of
the functional representation of various subclasses of LAA's are an
important part of the theory. The main result of the paper is a
stronger version of the functional representation theorem for locally
finite LAA's, the algebraic analogue of the completeness theorem of
lambda calculus.
Regimantas Pliuskevicius.
On saturated calculi for a linear temporal logic.
A new type of finitary and infinitary sequential calculi (named the
saturated ones) for a linear temporal logic is introduced. Instead of
induction-like postulates the saturated calculi contain some
sequents, indicating the saturation of the derivation process in
these calculi.
Hermann Puhlmann.
The snack powerdomain for database semantics.
Recently the use of domain theory for a semantics of databases has
been proposed. To model set-valued structures in this framework, a
powerdomain construction will be needed. As an appropriate
construction a modification of the recently introduced snack
powerdomain is investigated and shown to be a free algebra. Moreover,
the construction preserves bounded completeness. A slight
modification of the snack powerdomain yields the scone powerdomain
which, additionally, is distributive. Both constructions promise to
bear fruit in the domain theoretic approach to database semantics.
Bernhard Reus and Thomas Streicher.
Verifying properties of module construction in type theory.
This paper presents a comparison between algebraic
specifications-in-the-large and a type theoretical formulation of
modular specifications, called deliverables}. It is shown that the
laws of module algebra can be translated into the deliverables
approach and can be proved there in the language of type theory. The
adequacy of the Extended Calculus of Constructions as a possible
implementation of type theory is discussed and it is explained how
the reformulation of the laws is influenced by this choice.
Peter Ruzicka and Juraj Waczulik.
On time-space trade-offs in dynamic graph pebbling.
Pebble game on dynamic graphs is studied as an abstract model for the
incremental computations. We investigate how the time T and/or space S
is changing according to the number m of insert-edge/delete-edge
operations on directed acyclic graphs. We present time-space
trade-off of the form T=\Theta({n^2 \over S+m}) for the standard
pebble game on permutation graphs of size n. In the case of the
minimal space an extreme (superpolynomial) explosion of the time can
be related to the small (unite) size change in the graph. When the
space is not minimal a significant (superpolynomial) time increase
can also be achieved relative to the small (slowly increasing) change
of the graph size.
Vladimiro Sassone, Mogens Nielsen, and Glynn Winskel.
Deterministic behavioural models for concurrency.
This paper offers three candidates for a deterministic,
noninterleaving behaviour model, which generalizes Hoare traces to
the noninterleaving situation. The three models are all proved
equivalent in the rather strong sense of being equivalent as
categories. The models are: deterministic labelled event structures,
generalized Mazurkiewicz trace languages, and deterministic languages
of pomsets.
David Scholefield, Hussein Zedan, and He Jifeng.
Real-time refinement: Semantics and application.
A refinement calculus for the development of real-time systems is
presented. The calculus is based upon a wide-spectrum language called
TAM (the Temporal Agent Model), within which both functional and
timing properties can be expressed in either abstract or concrete
terms. A specification oriented semantics for the language is given.
Program development is considered as a refinement process i.e. the
calculation of a structured program from an unstructured
specification. A calculus of decomposition is defined. An example
program is developed.
Bernhard Steffen and Carsten Weise.
Deciding testing equivalence for real-time processes with dense
time.
We present a decision algorithm for testing equivalence of real-time
systems with a dense time domain. Real-time systems are modelled by
timed graphs, while the decision algorithm uses "mutually refined"
timer region graphs. The mutual refinement is important for the
synchronization of the timers of different real-time systems. Key to
our decision algorithm is the fact that -- despite the dense time
domain -- testing can be reduced to Pi-bisimulation in very much the
same way as in the untimed case.
Werner Stephan and Andreas Wolpers.
A calculus for higher order procedures with global variables.
An arithmetically complete axiom system for Algol-like higher order
procedures with mode depth one is presented. Such procedures may refer
to an unbounded number of "hidden" program variables by the use of
procedural parameters. As a solution, we add additional read
procedures to the program which are used in pre- and postconditions
to refer to these "hidden" variables.
David Stevens.
Variable substitution with iconic combinators.
An iconic notation for combinators is introduced, and the extensions
of combinatory logic needed to work with it are developed. It is shown
how entire sets of combinators can be defined by just two rules: a
general abstraction rule, and a general reduction rule. These are the
only rules needed for variable substitution. It is suggested that the
technique may have advantages for implementing a functional language.
Ralf Treinen.
Feature constraints with first-class features.
Feature Constraint System have been defined elsewhere, providing a
record like notion for rational trees and extending Colmerauer's
rational tree constraint system. We extend the feature constraint
system of [ST92a] to variable features access $x[v]w$, where $v$ is a
variable ranging over feature symbols. We show that the
satisfiability problem of conjunctions of atomic constraints is
NP-complete. Satisfiability of quantifier-free constraints is shown
to be decidable, while the $\exists^\star\forall^\star\exists^\star$
fragment of the first order theory is undecidable.
R. J. van Glabbeek.
A complete axiomatization for branching bisimulation congruence of
finite-state behaviours.
This paper offers a complete inference system for branching
bisimulation congruence on a basic sublanguage of CCS for
representing regular processes with silent moves. Moreover, complete
axiomatizations are provided for the guarded expressions in this
language, representing the divergence-free processes, and for the
recursion-free expressions, representing the finite processes.
Furthermore it is argued that in abstract interleaving semantics (at
least for finite processes) branching bisimulation congruence is the
finest reasonable congruence possible. The argument is that for
closed recursion-free process expressions, in the presence of some
standard process algebra operations like partially synchronous
parallel composition and relabelling, branching bisimulation
congruence is completely axiomatized by the usual axioms for strong
congruence together with Milner's first tau-law a tau X = aX.
Dorothea Wagner and Frank Wagner.
Between min cut and graph bisection.
We investigate a class of graph partitioning problems whose two
extreme representatives are the well-known Min Cut and Graph
Bisection problems. The former is known to be efficiently solvable by
flow techniques, the latter to be NP-complete. The results presented
in this paper are
-- a monotony result of the type "The
more balanced the partition we look for has to be, the harder the problem".
-- a complexity result clarifying the status of a large part of
intermediate problems in the class.
Thus we show the existence and partly localize an "efficiency
border" between the two extremes.
Egon Wanke.
Paths and cycles in finite periodic graphs.
We consider finite periodic graphs} G^m defined by nonnegative
integer vectors m and directed graphs G whose edges are labeled
with integer vector-weights. G^m has vertex set
V \times \{x |\vec{0}\leq x\leq m\} , and an edge from (u,x) to (v,x+z)
iff G has an edge from u to v with vector weight z. We show that
path and cycle problems for finite periodic graphs are
PSPACE-complete under various restrictions, but solvable in
polynomial time if the vector weights of the edges are bounded.
Jilei Yin and Hong Zhu.
Learning decision lists from noisy examples.
In the paper we solve an open problem raised by Rivest, show that the
concept class k-Decision lists can be learned, in the sense of
Valiant, from random examples with classification noise.
Nicolas Zabel.
Analytic tableaux for finite and infinite Post logics.
We present a tableau-based calculus for the finite and infinite
valued Post logics, well suited for automated deduction. We define a
possible world semantics and a prefixed tableau calculus with
unification on this basis. The world-information is handled by
solving constraints which express ordering problems. This calculus is
advantageously compared with other existing ones.
********************************************************************