From honeydew.srv.cs.cmu.edu!crabapple.srv.cs.cmu.edu!fp Tue Sep 21 13:49:02 EDT 1993
Article: 8581 of comp.lang.prolog
Xref: honeydew.srv.cs.cmu.edu comp.lang.prolog:8581
Newsgroups: comp.lang.prolog
Path: honeydew.srv.cs.cmu.edu!crabapple.srv.cs.cmu.edu!fp
From: fp+@cs.cmu.edu (Frank Pfenning)
Subject: CFP: Logic Programming and Automated Reasoning (LPAR'94)
Message-ID:
Keywords: conference, logic programming, automated reasoning
Sender: news@cs.cmu.edu (Usenet News System)
Nntp-Posting-Host: alonzo.tip.cs.cmu.edu
Organization: School of Computer Science, Carnegie Mellon
Date: Mon, 20 Sep 1993 15:52:06 GMT
Lines: 79
Announcement and Call for Papers
5th International Conference on
Logic Programming and Automated Reasoning (LPAR'94)
Kiev, Ukraine, July 16-21, 1994
LPAR'94 welcomes submissions in all areas of logic programming and automated
reasoning, including (but not limited to): analysis, synthesis and
verification; applications; classical and non-classical logics; constraints;
constructive theorem proving; deductive databases; functions and equations;
higher-order and meta-programming; implementation and architectures; inductive
theorem proving; logical frameworks; parallelism and concurrency; proof theory
and semantics; rewriting; theorem proving and symbolic computation; types and
type theory; unification. Papers submitted to this conference must contain
material not previously published, presented at a conference, or
simultaneously submitted elsewhere. Authors should submit 6 copies of a full
draft paper to the program chair by January 14, 1994. From countries where
copying may be a problem one copy will be sufficient. All papers must be
written in English. The length of the paper must not exceed 15 pages
following the Springer-Verlag Lecture Notes series format (approx. 13x20cm in
10pt font). Guidelines and an appropriate LaTeX style file are available from
the program chair. Proceedings of previous LPAR conferences were published as
Springer-Verlag LNAI 592, 624, and 698. Submissions should be accompanied by
an electronic mail message to lpar94@cs.cmu.edu, containing title, complete
contact information, and abstract.
In addition to contributed papers, the conference will feature some invited
speakers, several tutorials, and system demonstrations. The conference
will once again be held aboard a ship and include some excursions.
Program Committee
David Basin, MPI Saarbruecken
Antonio Brogi, University of Pisa
Philippe Codognet, INRIA Rocquencourt
Saumya Debray, University of Arizona
Melvin Fitting, Lehmann College
Steffen Hoelldobler, TH Darmstadt
Masami Hagiya, University of Tokyo
Michael Hanus, MPI Saarbruecken
Claude Kirchner, INRIA Lorraine & CRIN
Jack Minker, University of Maryland
Grigori Mints, Stanford
Tobias Nipkow, TU Munich
Christine Paulin-Mohring, ENS Lyon
Frank Pfenning, Carnegie Mellon University
Lutz Pluemer, University of Bonn
Vladimir Sazonov, PSI Pereslavl-Zalesski, Russia
Danny de Schreye, Catholic University Leuven
Dana Scott, Carnegie Mellon University
Gert Smolka, DFKI Saarbruecken
Sergei Soloviev, Aarhus University
Konstantin Vershinin, Institute of Cybernetics, Kiev
Andrei Voronkov, University of Uppsala
Mark Wallace, ECRC Munich
Lincoln Wallen, Oxford University
Program Chair Local Arrangements
Frank Pfenning / LPAR'94 Andrei Voronkov
Department of Computer Science Computer Science Department
Carnegie Mellon University University of Uppsala
Pittsburgh, PA 15213-3891, U.S.A. Polacksbacken 1, Box 311
+1 412 268 6343 S 751 05 Uppsala, Sweden
lpar94@cs.cmu.edu voronkov@csd.uu.se
Important Dates Organizing Committee
Submission: January 14, 1994 Eugene Dantsin (co-chair),
Konstantin Vershinin (co-chair),
Notification: March 14, 1994 Igor Romanenko, Andrei Voronkov,
Camera-Ready: April 20, 1994 Alexander Zhezherun
--
Frank Pfenning fp@cs.cmu.edu
Carnegie Mellon University Pittsburgh, Pennsylvania, USA
Article 4809 of news.announce.conferences:
Xref: crabapple.srv.cs.cmu.edu news.announce.conferences:4809
Newsgroups: news.announce.conferences
Path: crabapple.srv.cs.cmu.edu!honeydew.srv.cs.cmu.edu!magnesium.club.cc.cmu.edu!news.sei.cmu.edu!cis.ohio-state.edu!pacific.mps.ohio-state.edu!math.ohio-state.edu!cs.utexas.edu!uunet!sparky!rick
From: fp+@cs.cmu.edu (Frank Pfenning)
Subject: CFP: Logic Programming and Automated Reasoning (LPAR'94)
Message-ID: <1993Sep30.172539.5371@sparky.sterling.com>
Keywords: conference, logic programming, automated reasoning
Sender: rick@sparky.sterling.com (Richard Ohnemus)
Organization: School of Computer Science, Carnegie Mellon
Date: Thu, 30 Sep 1993 17:25:39 GMT
Approved: rick@sparky.sterling.com
Expires: Sat, 15 Jan 1994 08:00:00 GMT
Lines: 79
X-Md4-Signature: 6cfbfe75d93d87727367f196d8c22ea0
Announcement and Call for Papers
5th International Conference on
Logic Programming and Automated Reasoning (LPAR'94)
Kiev, Ukraine, July 16-21, 1994
LPAR'94 welcomes submissions in all areas of logic programming and automated
reasoning, including (but not limited to): analysis, synthesis and
verification; applications; classical and non-classical logics; constraints;
constructive theorem proving; deductive databases; functions and equations;
higher-order and meta-programming; implementation and architectures; inductive
theorem proving; logical frameworks; parallelism and concurrency; proof theory
and semantics; rewriting; theorem proving and symbolic computation; types and
type theory; unification. Papers submitted to this conference must contain
material not previously published, presented at a conference, or
simultaneously submitted elsewhere. Authors should submit 6 copies of a full
draft paper to the program chair by January 14, 1994. From countries where
copying may be a problem one copy will be sufficient. All papers must be
written in English. The length of the paper must not exceed 15 pages
following the Springer-Verlag Lecture Notes series format (approx. 13x20cm in
10pt font). Guidelines and an appropriate LaTeX style file are available from
the program chair. Proceedings of previous LPAR conferences were published as
Springer-Verlag LNAI 592, 624, and 698. Submissions should be accompanied by
an electronic mail message to lpar94@cs.cmu.edu, containing title, complete
contact information, and abstract.
In addition to contributed papers, the conference will feature some invited
speakers, several tutorials, and system demonstrations. The conference
will once again be held aboard a ship and include some excursions.
Program Committee
David Basin, MPI Saarbruecken
Antonio Brogi, University of Pisa
Philippe Codognet, INRIA Rocquencourt
Saumya Debray, University of Arizona
Melvin Fitting, Lehmann College
Steffen Hoelldobler, TH Darmstadt
Masami Hagiya, University of Tokyo
Michael Hanus, MPI Saarbruecken
Claude Kirchner, INRIA Lorraine & CRIN
Jack Minker, University of Maryland
Grigori Mints, Stanford
Tobias Nipkow, TU Munich
Christine Paulin-Mohring, ENS Lyon
Frank Pfenning, Carnegie Mellon University
Lutz Pluemer, University of Bonn
Vladimir Sazonov, PSI Pereslavl-Zalesski, Russia
Danny de Schreye, Catholic University Leuven
Dana Scott, Carnegie Mellon University
Gert Smolka, DFKI Saarbruecken
Sergei Soloviev, Aarhus University
Konstantin Vershinin, Institute of Cybernetics, Kiev
Andrei Voronkov, University of Uppsala
Mark Wallace, ECRC Munich
Lincoln Wallen, Oxford University
Program Chair Local Arrangements
Frank Pfenning / LPAR'94 Andrei Voronkov
Department of Computer Science Computer Science Department
Carnegie Mellon University University of Uppsala
Pittsburgh, PA 15213-3891, U.S.A. Polacksbacken 1, Box 311
+1 412 268 6343 S 751 05 Uppsala, Sweden
lpar94@cs.cmu.edu voronkov@csd.uu.se
Important Dates Organizing Committee
Submission: January 14, 1994 Eugene Dantsin (co-chair),
Konstantin Vershinin (co-chair),
Notification: March 14, 1994 Igor Romanenko, Andrei Voronkov,
Camera-Ready: April 20, 1994 Alexander Zhezherun
--
Frank Pfenning fp@cs.cmu.edu
Carnegie Mellon University Pittsburgh, Pennsylvania, USA
Article 9265 of comp.lang.prolog:
Xref: glinda.oz.cs.cmu.edu comp.lang.prolog:9265 comp.ai:20074
Newsgroups: comp.lang.prolog,comp.ai
Path: honeydew.srv.cs.cmu.edu!fp
From: fp+@cs.cmu.edu (Frank Pfenning)
Subject: 2nd CFP: LPAR'94
Message-ID:
Keywords: conferences, call for papers, logic programming, automated reasoning
Sender: news@cs.cmu.edu (Usenet News System)
Nntp-Posting-Host: alonzo.tip.cs.cmu.edu
Organization: School of Computer Science, Carnegie Mellon
Date: Tue, 28 Dec 1993 21:55:58 GMT
Lines: 80
Note the firm submission deadline of JANUARY 14!
Announcement and Call for Papers
5th International Conference on
Logic Programming and Automated Reasoning (LPAR'94)
Kiev, Ukraine, July 16-21, 1994
LPAR'94 welcomes submissions in all areas of logic programming and automated
reasoning, including (but not limited to): analysis, synthesis and
verification; applications; classical and non-classical logics; constraints;
constructive theorem proving; deductive databases; functions and equations;
higher-order and meta-programming; implementation and architectures; inductive
theorem proving; logical frameworks; parallelism and concurrency; proof theory
and semantics; rewriting; theorem proving and symbolic computation; types and
type theory; unification. Papers submitted to this conference must contain
material not previously published, presented at a conference, or
simultaneously submitted elsewhere.
Authors should submit 6 copies of a full draft paper to the program chair by
January 14, 1994. This is a firm deadline: papers received after this
deadline will not be considered. From countries where copying may be a
problem one copy will be sufficient. All papers must be written in English.
The length of the paper must not exceed 15 pages following the Springer-Verlag
Lecture Notes series format (approx. 13x20cm in 10pt font). Guidelines and an
appropriate LaTeX style file are available from the program chair.
Proceedings of previous LPAR conferences were published as Springer-Verlag
LNAI 592, 624, and 698. Submissions should be accompanied by an electronic
mail message to lpar94@cs.cmu.edu, containing title, complete contact
information, and abstract.
In addition to contributed papers, the conference will feature some invited
speakers, several tutorials, and system demonstrations. The conference will
once again be held aboard a ship and include some excursions.
Program Committee
David Basin, MPI Saarbr"ucken
Antonio Brogi, University of Pisa
Philippe Codognet, INRIA Rocquencourt
Saumya Debray, University of Arizona
Melvin Fitting, Lehmann College
Steffen H"olldobler, TU Dresden
Masami Hagiya, University of Tokyo
Michael Hanus, MPI Saarbr"ucken
Claude Kirchner, INRIA Lorraine
Jack Minker, University of Maryland
Grigori Mints, Stanford
Tobias Nipkow, TU Munich
Christine Paulin-Mohring, ENS Lyon
Frank Pfenning, Carnegie Mellon University
Lutz Pl"umer, University of Bonn
Vladimir Sazonov, PSI Pereslavl-Zalesski, Russia
Danny de Schreye, Catholic University Leuven
Dana Scott, Carnegie Mellon University
Gert Smolka, DFKI Saarbr"ucken
Sergei Soloviev, Aarhus University
Konstantin Vershinin, Institute of Cybernetics, Kiev
Andrei Voronkov, University of Uppsala
Mark Wallace, ECRC Munich
Lincoln Wallen, Oxford University
Program Chair Local Arrangements
Frank Pfenning / LPAR'94 Andrei Voronkov
Department of Computer Science Computer Science Department
Carnegie Mellon University University of Uppsala
Pittsburgh, PA 15213-3891, U.S.A. Polacksbacken 1, Box 311
+1 412 268 6343 S 751 05 Uppsala, Sweden
lpar94@cs.cmu.edu voronkov@csd.uu.se
Important Dates Organizing Committee
Submission: January 14, 1994 Eugene Dantsin (co-chair),
(firm deadline!) Konstantin Vershinin (co-chair),
Notification: March 14, 1994 Anatoli Degtyarev, Igor Romanenko,
Camera-Ready: April 20, 1994 Andrei Voronkov, Alexander Zhezherun
--
Frank Pfenning fp@cs.cmu.edu
Carnegie Mellon University Pittsburgh, Pennsylvania, USA
Article 10357 of comp.lang.prolog:
Xref: glinda.oz.cs.cmu.edu comp.lang.prolog:10357
Newsgroups: comp.lang.prolog
Path: honeydew.srv.cs.cmu.edu!fp
From: fp+@cs.cmu.edu (Frank Pfenning)
Subject: LPAR'94 Program and Registration
Message-ID:
Sender: news@cs.cmu.edu (Usenet News System)
Nntp-Posting-Host: alonzo.tip.cs.cmu.edu
Organization: School of Computer Science, Carnegie Mellon
Date: Fri, 29 Apr 1994 13:11:34 GMT
Lines: 576
PROGRAM AND REGISTRATION INFORMATION
Fifth International Conference on
Logic Programming and Automated Reasoning (LPAR'94)
July 16-22, 1994, Kiev, Ukraine
CONFERENCE PROGRAM
Saturday, July 16
Noon-Midnight Boarding of "Marshal Koshevoi"
19:00 Welcome Reception
Sunday, July 17
Invited Tutorial 1
9:00-11:00 The Calculus of Inductive Definitions and its Implementation:
the Coq Proof Assistant
Christine Paulin-Mohring, ENS Lyon
--- Break ---
11:30-12:00 Generalization and Reuse of Tactic Proofs
Amy Felty and Douglas Howe (AT&T, Murray Hill)
12:00-12:30 Program Tactics and Logic Tactics
Fausto Giunchiglia (IRST, Trento)
and Paolo Traverso (University of Trento)
--- Lunch ---
14:30-15:00 On the Relation between the Lambda-Mu-Calculus and the
Syntactic Theory of Sequential Control
Philippe de Groote (INRIA-Lorraine, Nancy)
15:00-15:30 On a Proof-Theoretical Analysis of Sigma-1-1-AC, Sigma-1-1-DC
and Delta-1-1-CA
Sergei Tupailo (Stanford University)
--- Break ---
Invited Tutorial 2
16:00-18:00 Problem Solving by Quantifier Elimination
Hoon Hong (RISC, Linz)
Monday, July 18
Invited Talk
9:00-10:00 Manuel Hermenegildo, Universidad Politecnica de Madrid
Some Fundamental Principles in Parallel Execution
of Logic and Constraint Logic Programs
--- Break ---
10:30-11:00 Proof Plans for the Correction of False Conjectures
Raul Monroy, Alan Bundy, and Andrew Ireland
(University of Edinburgh)
11:00-11:30 On the Value of Antiprenexing
Uwe Egly (Technical University Darmstadt)
--- Break ---
12:00-12:30 Implementing a Finite-Domain CLP-Language on Top of Prolog:
a Transformational Approach
Henk Vandecasteele and Danny De Schreye (KU Leuven)
12:30-13:00 RISC-CLP(CF) Constraint Logic Programming over Complex Functions
Hoon Hong (RISC, Linz)
--- Lunch ---
14:30-15:00 Logical Closures
Dominic Duggan (University of Waterloo)
15:00-15:30 Higher-Order Rigid E-Unification
Jean Goubault (Bull Corporate Research, Les Clayes sous Bois)
--- Break ---
Invited Tutorial 3
16:00-18:00 Negation in Logic Programming
Krzysztof R. Apt (CWI) and
Roland Bol (Eindhoven University of Technology)
Tuesday, July 19
Invited Talk
9:00-10:00 Michel Parigot (Universite Paris 7)
On Extensions of the Paradigm ``Proofs-as-Programs''
to Classical Logic
--- Break ---
10:30-11:00 Program Extraction in a Logical Framework Setting
Penny Anderson (INRIA, Sophia-Antipolis)
11:00-11:30 Higher-Order Abstract Syntax with Induction in Coq
Joelle Despeyroux (INRIA, Sophia-Antipolis) and
Andre Hirschowitz (CNRS, University of Nice)
--- Break ---
12:00-12:30 Towards Efficient Calculi for Resource-Oriented Deductive Planning
Stefan Bruning (Technical University Darmstadt)
12:30-13:00 A Logic Programming Framework for the Abductive
Inference of Intentions in Cooperative Dialogues
Paulo Quaresma and Jose Gabriel Lopes (UNINOVA, Portugal)
--- Lunch ---
Afternoon Excursion
19:00 Conference Dinner
Wednesday, July 20
Invited Talk
9:00-10:00 Andrei Voronkov (University of Uppsala)
The Anatomy of Vampire:
New Directions in Efficient Implementation of Logical Inference
--- Break ---
10:30-11:00 Constraint Logic Programming in the Sequent Calculus
John Darlington and Yike Guo (Imperial College, London)
11:00-11:30 On conditional rewrite systems with extra variables
and deterministic logic programs
Jurgen Avenhaus and Carlos Loria-Saenz
(University of Kaiserslautern)
--- Break ---
12:00-12:30 A Bottom-up Reconstruction of the Well-founded
Semantics for Disjunctive Logic Programs
Cristian Papp (University Al I Cuza, Iasi, Romania)
12:30-13:00 An Efficient Computation of the Extended Generalized
Closed World Assumption by Support-for-Negation Sets
Dietmar Seipel (University of Tubingen)
--- Lunch ---
14:30-15:00 Multi-SLD Resolution
Donald A. Smith (University of Waikato, New Zealand) and
Timothy Hickey (Brandeis University, Massachusetts)
15:00-15:30 On Anti-Links
Bernhard Beckert, Reiner Hahnle (University of Karlsruhe),
Anavai Ramesh, and Neil V. Murray (SUNY at Albany)
--- Break ---
Invited Tutorial 4
16:00-18:00 Representing Knowledge in Extensions of Logic Programming Languages
Michael Gelfond (University of Texas at El Paso)
Thursday, July 21
9:00- 9:30 A Generic Declarative Diagnoser for Normal Logic Programs
Lunjin Lu (University of Birmingham)
9:30-10:00 Goal Dependent vs Goal Independent Analysis of Logic Programs
M. Codish (Ben-Gurion University, Israel),
M. Garcia de la Banda (Universidad Politecnica, Madrid)
M. Bruynooghe (KU Leuven),
and M. Hermenegildo (Universidad Politecnica, Madrid)
--- Break ---
10:30-11:00 A Kind of Achievement by Parts Method
Ph. Mathieu and J.P. Delahaye (CNRS, Universite de Lille)
11:00-11:30 Projection in Temporal Logic Programming
Zhenhua Duan, Maciej Koutny, and Chris Holt
(University of Newcastle upon Tyne)
--- Lunch ---
14:30-19:00 Afternoon Workshops and Demonstrations (TBA)
Friday, July 22
9:00-11:00 Morning Workshops and Demonstrations (TBA)
11:00-12:00 Deboarding the "Marshal Koshevoi"
Conference Ends
INVITED TUTORIAL 1
The Calculus of Inductive Definitions
and its Implementation:
the Coq Proof Assistant
Christine Paulin-Mohring
LIP/ENS Lyon
cpaulin@lip.ens-lyon.fr
Type Theory serves as a basis for several environments dedicated to the
formalization of reasoning. We shall present the theory and practice of
one of them: the Coq Proof Assistant.
This environment is based on a typed lambda-calculus called the Calculus
of Inductive Definitions. It is a powerful language which extends the
Calculus of Constructions, introduced by Coquand and Huet, with a
mechanism for general inductive definitions in the spirit of
Martin-Lof's Intuitionistic Type Theory.
The Coq proof assistant can be decomposed into three parts.
o A specification language which combines higher-order logic,
functional programming and inductive definitions of relations.
o A tactic language which provides several tools for the
interactive development of proofs of formulas.
o An environment for manipulating proof-terms built by the
system, especially for extracting ML programs out of constructive
proofs of specifications.
INVITED TUTORIAL 2
Problem Solving by Quantifier Elimination
Hoon Hong
Research Institute for Symbolic Computation
Johannes Kepler University, Linz
hhong@risc.uni-linz.ac.at
The tutorial consists of two parts:
(1) We describe and illustrate the following view:
"Many non-trivial problem solving processes are essentially
quantifier elimination (qe) processes. In fact, it (qe) is a core
of constructive mathematics and computer science. Thus
automating problem solving usually amounts to devising methods
for quantifier elimination."
(2) We describe a few quantifier elimination algorithms for the
first order theory of real numbers (formally called real closed
fields). We give several examples of their use in solving
various problems. If time allows, we give a survey of other
theories that also admit quantifier elimination.
INVITED TUTORIAL 3
Negation in Logic Programming
Krzysztof R. Apt Roland Bol
Mathematics and Computer Science Mathematics and Computer Science
CWI & University of Amsterdam Eindhoven University of Technology
apt@cwi.nl bol@win.tue.nl
The use of negation in logic programming has been thoroughly studied
over the last 15 years. One of its interesting features is that it can
naturally support non-monotonic reasoning. The aim of this tutorial is
to provide an overview of the main developments in the proof theory and
model theory of logic programming with negation, and on the relationship
between them. More specifically, we shall discuss the SLDNF- and
SLS-resolution procedures and their modification by means of tabulation,
and various 2-valued and 3-valued semantics, including Clark's
completion, stable model and well-founded semantics.
INVITED TUTORIAL 4
Representing Knowledge in Extensions of Logic Programming Languages
Michael Gelfond
Computer Science Department
University of Texas at El Paso
mgelfond@cs.ep.utexas.edu
In this tutorial I'll describe some recent work aimed at the application
of declarative logic programming to knowledge representation. This
includes a description of an extension of definite logic programs by
classical (explicit) negation, disjunction and modal operators and of
the semantics of this language. We will also discuss a methodology of
the use of the language for representing various forms of commonsense
reasoning and mathematical properties of programs needed to support this
methodology.
LOCATION
========
The conference will be held aboard the ship "Marshal Koshevoi" which
will cruise on the Dnieper, starting and ending in Kiev, the capital of
the Ukraine. Kiev has an international airport and is accessible by
most major international airlines. All visitors will be required to
obtain a visa in advance of the trip; please contact a local embassy or
consulate. It is recommended that visitors bring only US Dollars which
are widely accepted. They should be exchanged to local currency in Kiev
only as needed. Credit cards are only accepted at a few restaurants and
hotels in Kiev, and not on the ship.
The weather in the Kiev area in the middle of July should be pleasant,
with little rain and temperatures around 25 C (75 F). Neither email nor
telephone contact will be available on board. The ship will make daily
stops, with an excursion planned for the afternoon of Tuesday, July 19
in Zaporozhie. The ship can be boarded any time between noon and
midnight on Saturday, July 16. The ship returns to Kiev on Thursday,
July 21, but accomodation will still be booked until July 22. The ship
must be deboarded by 11am on July 22.
The organizers will try to arrange for transportation from the airport
and train station to the dock. If it is not available when you arrive
you should use only an official taxi. The fare should be negotiated and
should be around 15 to 20 US Dollars.
In case of problems you can reach the local organizers, Anatoli
Degtyarev and Igor' Romanenko at (+7 044) 2663108 in Kiev.
SYSTEM DEMONSTRATIONS
=====================
Some PC's and possibly a Sun SparcStation will be available for system
demonstrations which will be arranged informally during the conference.
Please contact the local arrangements chair at voronkov@csd.uu.se for
further information.
LOCAL ORGANIZATION
==================
Please address registration form and inquiries to:
Andrei Voronkov
Computing Science Department
University of Uppsala
Polacksbacken 1, Box 311
S 751 05 Sweden
Email: voronkov@csd.uu.se
Phone: +46 18 181055, +46 18 422376
FAX: +46 18 511925, +46 18 422376
REGISTRATION AND ACCOMODATION
=============================
The registration form should be sent to the local arrangement chair
above and must include full payment. The registration fee includes
conference participation, a copy of the proceedings, and meals and
lodging aboard the ship. Each participant will occupy his or her own
cabin. There will be no separate charges for accomodation or meals
during the conference.
Payment can be made either by cheque in German marks or by a bank
transfer. Cheques must be sent to the local chair at the same address.
(Warning: please do NOT send cheques directly to the bank.) If you use
a bank transfer please send a copy of the bank transfer form to this
address. Please check that all transfer fees have been paid by the
sender. Cheques must be drawn at a German bank and made payable to
Tatiana Rybina -- LPAR. The account details are the following.
Account number: 43 22 764.
Address: Deutsche Bank; Filiale M\"unchen
Zweigstelle Max-Weber-Platz
Max-Weber-Platz 11
D 81675 Munich
Germany
Bank code: 700 700 10
Telephone +49-89-473088
Telefax +49-89-4707445
In case of cancellation of registration, the organizing committee should
be notified in writing or by email. If the cancellation is received
before June 1, 1994, a full refund will be given. For cancellations
received after June 1, 1994, no refund will be possible.
All payments must be received by June 1, 1994.
LPAR'94 REGISTRATION FORM
=========================
Last Name __________________________________________________
First Name _________________________________________________
Affiliation ________________________________________________
Street Address _____________________________________________
_______________________________________________________
City & Postal Code _________________________________________
Country ____________________________________________________
Phone(s) ___________________________________________________
Fax ________________________________________________________
E-mail _____________________________________________________
REGISTRATION RATES. The fees below are in DM. Circle the
appropriate fields below. The additional late registration fee
of DM 150 must be payd in case when payments are made after
June 1. There is no registration fee for accompanying persons.
Accomodation and meals DM 135 x 6 nights = DM 810 ____
Registration (regular/student) DM 450/250 ____
Additional late registration DM 150 ____
Tutorial 1 DM 30 ____
Tutorial 2 DM 30 ____
Tutorial 3 DM 30 ____
Tutorial 4 DM 30 ____
--------------------------------------------------------------
Total DM
Full-time student at ________________________________________
Form of Payment (circle one): Transfer Cheque
INVITED TALK
Some Fundamental Principles
in Parallel Execution
of Logic and Constraint Logic Programs
Manuel Hermenegildo
Facultad de Informatica
Universidad Politecnica de Madrid
herme@fi.upm.es
In this talk we attempt to view the parallel execution of logic
programming systems and concurrent logic programming systems, and their
respective generalization to constraint programming, from a new
perspective. We propose a new way of studying these systems, based on a
particular definition of parallelism. We argue that, under the given
assumptions, a large number of actual systems and models can be
classified and explained through the application, at different levels of
granularity, of only a few fundamental principles, such as:
o independence, (also referred to as stability) which
allows parallelism among non-deterministic threads,
o determinacy, which allows parallelism among dependent threads,
o non-failure, which allows guaranteeing non-speculativeness, and
o granularity, which allows guaranteeing speedup in the
presence of overheads.
Furthermore, we will argue, and support with examples, that this new
view allows easily transferring ideas across different proposals. Also,
and based on the convergence of concepts that this view brings, we will
propose a unified approach to the implementation of all these parallel
systems by using a common abstract machine. We also propose a model --
the CIAO Model (Concurrent, Constraint, Independence-based
And-/Or-Parallel Model) -- as a driver for these ideas.
INVITED TALK
On Extensions of the Paradigm ``Proofs-as-Programs''
to
Classical Logic
Michel Parigot
Universite Paris 7
parigot@logique.jussieu.fr
After two decades of intensive studies of the computational aspects of
intuitionistic systems through the so-called Curry-Howard isomorphism,
relating intuitionistic proofs to functional programs, a new research
topic appeared in the last few years: the extension of this isomorphism
to classical proofs. The extension appeared both from logical and
programming considerations:
o In the computational interpretations of intuitionistic logic, programs
are represented by proofs and computation is represented by some kind of
cut-elimination (or normalisation) procedure. The cut-elimination
mechanism being also defined for classical logic, it was natural to
consider it as a computation mechanism in this context too, and several
such computational interpretations of classical logic have been
proposed.
o In functional programming languages, the purely functional character
of programs appeared soon as an obstacle to practical programming.
Functional programming languages have thus been enriched, in different
ways, with control operators, like call/cc in Scheme. The theory of
these control operators, lambda-C-calculus, has been made by Felleisen,
and Griffin has remarked that they can be typed using some form of
classical logic.
The new phenomenon which appears with this extension is some kind of
non-determinism: computational interpretations of classical logic seem
to lead directly to non-confluent calculi. There are at least two
different ways to tackle this phemomenon: either to try to avoid
non-confluence by chosing some appropriate confluent sub-calculus, or to
try to use non-confluence in order to build a new non-deterministic
computational model.
In this talk we intend to:
o analyse the sources of non-confluence of the computational
interpretations of classical logic;
o compare different possible restrictions to confluent calculi (are
some of them better than the others? do they significantly differ from
those obtained by translations into intuitionistic logic?);
o to discuss the meaning and the possible uses of the non-determinism
associated to classcal proofs.
INVITED TALK
The Anatomy of Vampire:
New Directions in Efficient Implementation of Logical Inference
Andrei Voronkov
Computer Science Department
University of Uppsala
voronkov@csd.uu.se
We discuss an implementation technique, called code trees, for a class
of bottom-up procedures. It is applicable to many procedures, including
resolution-based procedures, the inverse method, bottom-up evaluation of
logic programs and theorem proving methods which use lemmaizing. Our
theorem prover Vampire implements several procedures as code trees.
Vampire is considerably faster than Otter, when both use the same
logical methods.
Code trees unify many ideas used in the implementation of logics, for
example abstract machines, indexing and binary decision diagrams. It is
a general methodology rather than an ad hoc technique. We show how the
consistent use of this methodology helped us in finding new indexing
schemes and in implementing bottom-up procedures on the ``set at a
time'' basis.
LPAR'94 ORGANIZATION
PROGRAM CHAIR
Frank Pfenning
LOCAL ARRANGEMENTS
Andrei Voronkov
PROGRAM COMMITTEE
David Basin, Antonio Brogi, Philippe Codognet, Saumya Debray, Melvin
Fitting, Steffen Holldobler, Masami Hagiya, Michael Hanus, Claude
Kirchner, Jack Minker, Grigori Mints, Tobias Nipkow, Christine
Paulin-Mohring, Frank Pfenning, Lutz Plumer, Vladimir Sazonov, Danny de
Schreye, Dana Scott, Gert Smolka, Sergei Soloviev, Konstantin Vershinin,
Andrei Voronkov, Mark Wallace, Lincoln Wallen
ORGANIZING COMMITTEE
Eugene Dantsin (co-chair), Konstantin Vershinin (co-chair),
Anatoli Degtyarev, Igor Romanenko, Andrei Voronkov, Alexander Zhezherun
--
Frank Pfenning fp@cs.cmu.edu
Carnegie Mellon University Pittsburgh, Pennsylvania, USA