LICS Newsletter 41

Newsletter 41

February 7, 1997




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