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