[Past issues of the newsletter are available at http://www.bell-labs.com/topic/conferences/lics/ and ftp://ftp.research.bell-labs.com/dist/lics/newsletters.] BOOK ANNOUNCEMENT The Classical Decision Problem E. Boerger, E. Graedel, Y. Gurevich Springer Verlag, 1996, 482 pp. (Perspectives in Mathematical Logic) ISBN 3-540-57073-X * This is the most complete and comprehensive treatment available in book form of the classical decision problem of mathematical logic and its role in modern computer science. A revealing analysis of the natural order of decidable and undecidable cases is given, and of particular interest to the reader will be the complete classification of the solvable and unsolvable standard cases of the classical decision problem, the complexity analysis of the solvable cases, the extremely comprehensive treatment of the reduction method, and the model-theoretic analysis of solvable cases. Many cases are treated here for the first time, and a great number of simple proofs and exercises have been included. The results and methods of the book have been used in logic, computer science & artifical intelligence. * Ordering information. See the URL above. BOOK ANNOUNCEMENT Resolution Proof Systems: An Algebraic Theory Zbigniew Stachniak Kluwer Academic Publishers, 1996 ISBN 0-7923-4017-5 * This book presents a new algebraic framework for the design and analysis of resolution based automated reasoning systems for a range of non-classical logics. It develops an algebraic theory of resolution proof systems focusing on the problems of proof theory, representation, and efficiency of the deductive process. A new class of logical calculi, the class of resolution logics, emerges as a second theme of the book. The logical and computational aspects of the relationship between resolution logics and resolution proof systems is explored in the context of monotonic as well as nonmonotonic reasoning. The book is aimed primarily at researchers and graduate students in Artificial Intelligence, Symbolic, and Computational Logic. The material is suitable either as a reference book for researchers or as a text book for a graduate course on the theoretical aspects of Automated Reasoning and Computational Logic. NEW PhD PROGRAM AT MUNICH (LMU AND TU) * Program. The Department of Mathematics of the Ludwig-Maximilians- Universitaet Muenchen and the Department of Computer Science of the Technischen Universitaet Muenchen (Germany) will establish a new postgraduate program ("Graduiertenkolleg") entitled "Logic in Computer Science" starting on April 1st, 1997. The aim is to extend the applicability of logical methods for design, specification, verification and optimization of programs, program systems and hardware. * Topics. Logical foundations: Lambda calculus, equational logic, temporal logic, model checking (Buchholz, Buettner, Clote, Kroeger, Nipkow, Schulz, Schwichtenberg). Theorem provers: integration of (higher order) equational logic, combination of theorem provers and special methods (Buchholz, Buettner, Clote, Kroeger, Nipkow, Schulz, Schwichtenberg). Modeling of distributed systems (Broy, Buettner, Kroeger, Wirsing). Specification and verification (Antreich, Broy, Clote, Kroeger, Nipkow, Schwichtenberg, Wirsing). Foundations of software technology (Antreich, Broy, Wirsing). * Grants. We offers 6 PhD grants for a period of maximally three years. * Applications. Applicants with very high qualification in one of the mentioned or related research topics are invited to send their applications with the usual documents (curriculum vitae, certifications, copies of master's thesis and publications, description of intended project, two letters of recommendation) not later than February 15th, 1997 to the chairman of the postgraduate program: Prof. Helmut Schwichtenberg, Mathematisches Institut der LMU, Theresienstr. 39, D-80333 Muenchen, Tel. +49 89 2394 4413/4, Fax +49 89 280 5248, E-mail: schwicht@rz.mathematik.uni-muenchen.de. ICLP'97 CALL FOR WORKSHOP PROPOSALS International Conference on Logic Programming July 8-11, 1997, Leuven, Belgium * Persons intending to organize a workshop at ICLP'97 are invited to submit a workshop proposal by January 15, 1997 by e-mail to iclp97@cs.kuleuven.ac.be. The workshop proposal should clearly indicate: the title of the workshop, the topics this title covers, discussion of the timeliness and relevance of the workshop, the name and e-mail address of the organizing persons, with indication of one of them as the workshop coordinator. ICLP'97 CALL FOR TUTORIAL PROPOSALS International Conference on Logic Programming July 8-11, 1997, Leuven, Belgium * Proposals are invited for tutorials to be held at ICLP'97. Persons interested in presenting a tutorial at ICLP'97 are invited to submit a tutorial proposal by February 27, 1997 by e-mail to iclp97@cs.kuleuven.ac.be. The tutorial proposal should include the title of the tutorial, a summary, stating the topics it covers, the name and e-mail address of the speaker, any required specific equipment, other than an overhead projector, duration of the tutorial (preferably 2 hours). NINTH INTERNATIONAL SCHOOL FOR COMPUTER SCIENCE RESEARCHERS Architecture Design and Validation Methods Lipari Island, 22 June - 5 July 1997 * The Ninth School for Computer Science Researchers addresses PhD students and young researchers who want to get exposed to the forefront of research activity in the field of "Architecture Design and Validation Methods". The school will be held in the beautiful surroundings of the Island of Lipari which can be reached by ferry from Naples, Milazzo, Messina, Reggio Calabria and Palermo. The official language is English. Students must follow six courses and choose three of them for the exam. A proficiency final exam at the end of each chosen course is mandatory. Saturday of the first week will be entirely dedicated to open research problems and discussion. * Application. A letter of application must be sent to Prof. Alfredo Ferro, Dipartimento di Matematica-Citta' Universitaria, Viale A. Doria, 6-95125, Catania, Italy, Fax: +39-95-330094, and must be received by April 20, 1997. The application should contain a c.v. plus at least two letters of recommendation but no papers. Students will be informed about acceptance by April 30, 1997.The registration fee for the school is 300 U.S. dollars per person. American students of the EAACSS consortium will be excused from payment of registration fees. * Courses. High Level Design (R. Camposano), Logic Synthesis and Optimization (G. De Micheli), Machine Assisted Verification (H. Eveking), Validation Methods (Z. Manna and E. Boerger), Layout design (R. Otten), Hw/Sw Co-Design (A. San Giovanni Vincentelli). 20th INTERNATIONAL WITTGENSTEIN SYMPOSIUM 10-16 August 1997 Kirchberg am Wechsel, Lower Austria * General Theme. The Role of Pragmatics in Contemporary Philosophy. * Sections. Pragmatic Aspects of Applied Logic. The Pragmatic Dimension of Language. Pragmatic Problems in the Philosophy of Science. Pragmatic Approaches in Ethics and in the Theory of Action. Pragmatic Philosophers and Pragmatic Systems of Thought. Wittgenstein. * Invited speakers. E. W. Adams, M. Bierwisch, D. Birnbacher, J. Bouveresse, J. Conant, P. Dick, L. Flores, P. Gaerdenfors, K. Gemes, P. Gochet, H. Haider, P. H. Hare, W. L. Harper, R. Hilpinen, R. C. Jeffrey, H. Kamp, H. Kreutz, T. Kuipers, N. Kurtonina, G. Meggle, P. Mittelstaedt, E. Morscher, D. Pears, J. L. Pollock, N. Rescher, E. von Savigny, E. Sidorenko, B. Skyrms, P. Suppes, R. Wojcicki. * Participation. If you want to participate, please contact by letter, fax or phone call: The Austrian Ludwig Wittgenstein Society, Congress Office, Markt 63, A-2880 Kirchberg am Wechsel, Austria, Europe, Telephone and Telefax: 01143 2641 2557. A detailed registration form will then be sent to you. BOOK ANNOUNCEMENT Specification of abstract data types J. Loeckx, H.-D. Ehrich, M. Wolf Wiley-Teubner, 1996 * The book provides an authoritative introduction to the mathematical foundations of algebraic program specification. Unlike most other publications on the subject, this book does not draw on category theory, but instead tries to demystify the topic and promote its use in practical applications. It clearly distinguishes between the study of algebras, logic, specification methods and specification languages and it avoids focusing on a particular logic or a particular specification method. After an informal discussion on the design of reliable software, the book presents the main notions and properties of algebras. Next it investigates logic, introducing a general notion of logic, encompassing those commonly used. On the basis of these fundamentals it describes in some detail three specification methods and the principles of specification languages. It concludes with a case study illustrating the use of abstract data type specification in software design. While treating the subject with mathematical precision, the book contains numerous examples, exercises and comments to provide a deeper understanding of concepts discussed. It was conceived as a student textbook but will also be a useful source of reference for researchers and developers using formal specification methods for software design. BOOK ANNOUNCEMENT Frontiers of combining systems Proceedings of the First International Workshop, Munich, March 1996 edited by F. Baader and K. U. Schulz Kluwer Academic Publishers Applied Logic Series 3 October 1996, 400 pp. ISBN 0-7923-4271-1 * The volume contains research papers that cover the combination of logics, the combination of constraint-solving techniques and decision procedures, the combination of deductive systems, the integration of data structures into Constraint Logic Programming formalisms, and logic modelling of multi-agent systems. These problems are addressed on different conceptual levels: from the investigation of formal properties of combined systems using methods of logic and mathematics to the consideration of physical connections and communication languages relavent for combination of software tools. SEVENTH INTERNATIONAL WORKSHOP ON LOGIC PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR'97) Leuven, Belgium, July 10-12, 1997 * Scope. Program specialisation and transformation, program synthesis, systematic program development in a declarative programming setting, focusing on logic programming in particular. * Submission. Extended abstracts (5-8 pages excluding references and appendices) must be submitted before April 18 either by e-mail (PostScript file to fuchs@ifi.unizh.ch), or 5 copies should be sent to Norbert E. Fuchs, Department of Computer Science, University of Zurich, CH-8057 Zurich, Switzerland. Submission of abstracts in PostScript by e-mail is preferred however, submissions in paper form are also possible. Submissions should include a return postal address and an e-mail address. Submissions will be reviewed by at least three members of the programme committee. Accepted abstracts will be collected into preliminary proceedings which will be available at the workshop. At least one author of each accepted abstract is expected to attend the workshop. INTERNATIONAL SUMMER SCHOOL Verification of Digital and Hybrid Systems An Advanced Study Institute of the NATO Science Committee May 26-June 6, 1997, Adora Golf Resort Hotel, Belek, Antalya, Turkey * Objective. The Summer School is a course of two weeks duration. The objective of the school is to expose in a systematic manner the recent advances in the formal verification of systems composed of both logical and continuous time components. The first week of the summer school shall focus on the issues involved in the formulation and the verification of the discrete event models. The issues involved cover theorem proving, system automaton models, logics, tools and complexity of verification techniques. The second part of the course shall explicitly deal with complex hybrid structures where discrete event models interact with continuous time control models. A paradigmatic case of such a hybrid system and associated verification issues is the example of smart cars moving on smart highways which shall constitute the case study of part 2. One clear objective of the summer school is to expose the interplay between two major disciplines of computer science and control theory in the context of hybrid systems. * Lectures will be given by: K. Inan, R. Kurshan, K. Mcmillan, J. Sifakis, P. Varaiya, R. Alur, C. Courcoubetis, A. Desphande, T. Henzinger, J. Moore, D. Peled, A. Pnueli, J. van Schuppen. * Application. For application form see the URL above or send mail to nato-asi@srdc.metu.edu.tr.