LICS Newsletter 46

Newsletter 49

January 2, 1998

[Past issues of the newsletter are available at 

  The Efficiency of Theorem Proving Strategies:
  A Comparative and Asymptotic Analysis
  David A. Plaisted and Yunshan Zhu
  ISBN: 3-528-05574-X
* This book introduces mathematical techniques for the analysis of the
  efficiencies of theorem proving strategies.  In particular, it
  develops techniques which permit one to estimate the sizes of the
  search spaces generated by theorem provers on various propositional
  and first-order problems.  Such an analysis helps to supplement
  empirical observations obtained by running provers on examples.
  This book should be of interest to those working in the fields of
  automated deduction, mathematical logic, artificial intelligence,
  and computational complexity.  This book gives asymptotic bounds on
  the sizes of the search spaces generated by many common first-order
  theorem proving strategies.  Thus it permits one to gain a
  theoretical understanding of the efficiencies of many different
  theorem proving methods.  This gives insight into the comparative
  advantages of various strategies, as well as suggesting new
  directions for research.  This book is aimed at students and
  researchers.  The book requires some mathematical sophistication or
  familiarity with analysis of algorithms.
* Ordering.  Informatica International, Inc, Department Vieweg, 275 C
  Marcus Blvd., Hauppage, New York 11788.  Phone: (516)952-1676, Fax:
  (516)952-1685, email:

  Queen Mary Westfield College, University of London
  May 10-13, 1998
* Invited speakers. Samson Abramsky, Chantale Berline, Martin Hyland,
  John McLean, David Pym.
* Special sessions. There will be two special sessions during the
  meeting.  The first of these will be devoted to security, while the
  second will be a session honoring Peter Landin.
* This is a workshop year for MFPS, which means that the remainder of
  the program will be made up of talks contributed by participants.
  The slots for these talks will be allotted on a first-come,
  first-served basis. If you are interested in attending the meeting
  and giving a talk, send email to including your
  name, the title of your talk and a short abstract.
* Organizing Committee. Stephen Brookes, Michael Main, Austin Melton,
  Michael Mislove, David Schmidt.  
* Co-chairmen for MFPS 14. Michael Mislove and Edmund Robinson.

  Advances in First-Order Theorem Proving
  Call for Papers
* Topics. Papers presenting original contributions in any area of
  first-order theorem proving are being sought for a special issue on
  `Advances in first-order theorem proving' of the Journal of Symbolic
  Computation.  Topics of interest include (but are not restricted
  to): resolution and tableau methods; equational reasoning and
  term-rewriting systems; constraint-based reasoning; unification
  algorithms for first-order theories; specialized decision
  procedures; propositional logic; abstraction; first-order
  constraints; complexity of theorem proving procedures; and
  applications of first-order theorem provers to problems in
  artificial intelligence, verification, and formal mathematics, as
  well as other areas.
* Submission.  Manuscripts should be unpublished works and not
  submitted elsewhere.  Revised and enhanced versions of papers
  published in conference proceedings that have not appeared in
  archival journals are eligible for submission.  The participants of
  FTP'97 are invited to submit papers, but the special issue is open
  for everybody.  All submissions will be subject to the standard
  review procedure.  Authors are invited to submit their manuscripts
  by e-mail to one of the Guest Editors as a PostScript file,
  preferably gzipped and uuencoded. The deadline for submissions is
  June 1, 1998.
* Guest editors.  Maria Paola Bonacina ( and
  Ulrich Furbach (

  Call for papers
  Freiburg, Germany, September 7 - 9, 1998
* Topics. Papers on current research in all aspects of Labeled
  Deduction are welcome, including but not limited to: Logical
  modeling based on Labeled Deduction; Formal metatheory for, or
  based on, Labeled Deduction; Hybrid reasoners and combinations of
  logics based on labeling; Automated reasoning, implementation, and
  system support; Annotated logic programming; Applications.
* Submissions. Email a postscript file, and a plain text file
  including title, authors, and contact information, to, before April 15, 1998.
* Organizing Committee. David Basin and Luca Vigano. 
* Program Committee. David Basin, Marcello D'Agostino, Dov Gabbay,
  Sean Matthews, Luca Vigano`. 

  Call for submissions
  Message from Edmund M. Clarke, Editor-in-Chief
* FORMAL METHODS IN SYSTEM DESIGN is in good health. Subscriptions are
  growing and the backlog for accepted papers is down.  The journal is
  now covered in Science Citation Index.  The 1997 issues are complete
  and on schedule.  You can view the table of contents for the new
  issues by accessing the publisher's web site at:
  The Editorial Board has been expanded and includes an outstanding
  array of research leaders.  The review process has been streamlined
  and papers are now going through the system quicker.
* We hope you will submit your next paper to Formal Methods in System
  Design. In order to find out information on how to submit papers to
  the journal, contact: Mrs. Judith Kemp, FORM--Editorial Office,
  Kluwer Academic Publishers, 101 Philip Drive, Assinippi Park,
  Norwell, Massachusetts 02061, Tel. 617-871-6300, Fax. 617-871-6528,

  Call for papers
  Nice, France, September 8-11, 1998
* Topics: The scope of CONCUR'98 covers all areas of semantics,
  logics, and verification techniques for concurrent systems.  A list
  of specific topics includes (but is not limited to) concurrency
  related aspects of models of computation and semantic domains,
  process algebras, Petri nets, event structures, real-time systems,
  hybrid systems, decidability, model-checking, verification
  techniques, refinement techniques, term and graph rewriting,
  distributed programming, logic constraint programming,
  object-oriented programming, typing systems and algorithms, case
  studies, tools and environments for programming and verification.
* Submissions: Summaries (up to 15 pages, typeset 12 points)
  must be received by March 10, 1998.  Authors will be
  notified of acceptance or rejection by May 8, 1998.  Electronic
  submissions are strongly encouraged; instructions may be found at
  the CONCUR'98 web page, or obtained by sending an email with subject
  `submission information' to the address
  If surface mail is used, then five (5) copies of the paper should be
  sent to the following address: Concur'98, INRIA Sophia-Antipolis, BP
  93, F-06902 Sophia-Antipolis Cedex, France.
* Program Committee: M. Abadi, A. Asperti, J. Bradfield, E. Clarke,
  R. de Simone (co-chair), J. Esparza, P. Gastin, R. van Glabbeek,
  G. Gonthier, M. Hennessy, O. Maler, F. Moller, U. Montanari,
  M. Mukund, M. Nielsen, P. Panangaden, J. Parrow, A. Rensink,
  D. Sangiorgi (co-chair), C. Talcott, J. Winkowski.
* Invited Talks: G. Berry, J.F. Groote, T. Henzinger, U. Herzog,
  B. Pierce, J. Rutten, J.-B. Stefani, M. Vardi.

  Call for papers
  Manchester, United Kingdom, 15 - 19 June 1998
* Topics. Specification, analysis, synthesis, verification,
  composition, reuse, transformation, schemas, specialization,
  industrial applications.
* Submissions.  Electronic submissions are strongly encouraged.  See
  the workshop homepage for full instructions regarding the formatting
  requirements and the electronic submission procedure.  Submission
  deadline is 27 March 1998.
* Program Committee.  Pierre Flener (chair), Nicoletta Cocco, Andreas
  Hamfelt, Kung-Kiu Lau, Baudouin Le Charlier, Michael Leusche,l
  Michael Lowry, Ali Mili, Lee Naish, Mario Ornaghi, Alberto
  Pettorossi, Dave Robertson, Richard Waldinger.

  Daghsthul seminar
  October 20-24, 1997
* The idea of organizing a Workshop on Applications of Tree Automata
  to Rewriting, Logic, and Programming came during the joint
  conference FLoC (Federated Logic Conference, New Brunswick, 1996),
  which brought together the Symposium on Logic in Computer Science,
  the Conference on Rewriting Techniques and Applications, the
  Conference on Automated Deduction and the Conference on
  Computer-Aided Verification. We realized there that, though logic
  was the straightforward intersection between these four communities,
  there were also common underlying themes and techniques of more
  specific nature.  An important example was ``applications of tree
  automata''.  This computational model is indeed used in various
  domains of applications which, to some extent, ignore each other.
  The goal of the workshop was to bring together researchers who are
  involved in such applications and to promote cross-fertilization of
  ideas which have been developed independently in different
  contexts.  So, automata techniques invented, e.g., in rewriting
  theory could also be useful in the context of typing or program
  analysis. On the other hand, approximation methods as used by the
  compiler people could also be successfully applied in practical
  theorem provers either to provide partial answers or to guide the
  actual proof engine. The workshop was supported by the European
  Community - TMR Program and by the National Science Foundation. 
* For a detailed description of the workshop, see the URL above. 
* Organizers: H. Comon, D. Kozen, H. Seidl, M.Y. Vardi.

  in conjunction with ACM SIGMOD/PODS '98
  Call for proposals
  Seattle, Washington, USA, May 31, 1998
* Constraints provide a flexible and uniform way to represent and
  manipulate diverse data capturing spatio-temporal behavior, complex
  modeling requirements, partial and incomplete data, and so on.  As a
  result, Constraint Database Systems and Constraint Languages have
  found considerable attention over the last years.  The objective of
  this informal workshop is to bring together practitioners and
  researchers to share and explore their views on constraint database
  technology and its applications. The main focus of the workshop will
  be to communicate and discuss recent results of research into
  Constraint Databases and to identify future research directions.
* The workshop will emphasize informal discussions between
  researchers, and therefore there will be no published proceedings. 
  Reports on work in progress, and papers already submitted or
  published elsewhere, are welcome. We expect that participation will
  be free for anyone registered for SIGMOD/PODS. 
* Invited speakers. Jean-Louis Lassez, Sridhar Ramaswamy, Dirk Van
  Gucht, Victor Vianu.  
* Submission. Proposals for talks on all aspects of constraint
  databases are welcome.  If you would like to give a presentation at
  the workshop, please send your proposal (in plain ASCII) to  Proposals are due on March 13, 1998. They
  should include the title, authors, name of the person who plans to
  give the talk, and a one page abstract.
* Organizing committee. Alex Brodsky, Volker Gaede, Gabriel Kuper,
  Leonid Libkin, Jianwen Su. 

  Research field: Knowledge Representation, Logic in Computer Science
  Department of Computer Science
  Aachen University of Technology, Germany
* The Department of Computer Science at the Aachen University of
  Technology, Germany, invites applications for a position within a
  research project funded by the Deutsche Forschungsgemeinschaft
  (DFG). The position is initially available for two years, starting
  March 1998, and it provides a salary corresponding to BAT IIa (about
  DM 5000 per month). A Ph.D. in Computer Science or a related field
  or a very good advanced degree in one of these fields (corresponding
  to the German "Diplom") is required. Applicants should have
  experience in logic and/or knowledge representation.  The project,
  which will be carried out in collaboration with the group of
  Prof. Graedel, is concerned with constructing decision procedures
  for and investigating the complexity of logical decision problems,
  with an emphasis on problems that are relevant in knowledge
  representation. On the one hand, formula classes with few variables
  and/or restricted quantification are of special importance. On the
  other hand, constructs have to be taken into account that are
  typically used in computer science applications (such as fixed
  points, transitive closures, counting quantifiers), but are not
  available in the classical framework of first-order logic. In
  addition to decision procedures for large classes of formulae we are
  also interested in optimized procedures for subclasses that are
  relevant in knowledge representation.
* Please send applications (preferably by Email and before January 10,
  1998) to: Prof. F. Baader, RWTH Aachen, Lehr- und Forschungsgebiet
  Theoretische Informatik, Ahornstr. 55, 52074 Aachen, Germany,
  E-mail:, phone: (++49 241)-8021131,
  fax: (++49 241)-8888360.

  RTA'98 Workshop & Tutorial, 31 March 1998    
  Call for Participation
* The aim of this workshop and tutorial is to provide an opportunity
  for the participants of RTA'98 to learn more about categorical term
  rewriting, and to provide a meeting place for researchers within the
  field to present and discuss new ideas where category theory can be
  fruitfully applied to rewriting.  The workshop and tutorial will
  occupy one afternoon of RTA'98. The tutorial will comprise
  introductory talks about the categorical concepts relevant to term
  rewriting, such as the theory of monads. For the workshop, talks are
  invited about work applying categorical or algebraic concepts to
  term rewriting or related areas, such as graph rewriting, string
  rewriting or unification.
* Submission deadline.  31 January 1998. For more information, see the
  URL above, or
* Organizers.  Neil Ghani, Christoph Lueth, Fer-Jan de Vries.

  Call for participation
  March 31 - April 2, 1998
  School of Mathematical and Computational Sciences, University of St Andrews
* Invited speakers.  Carolyn Brown, Rod Burstall, James Davenport,
  Abbas Edalat, Ian Gent, Leslie Goldberg, Angus Macintyre, Luke Ong,
  Rick Thomas.
* See the URL above for further information.

  Call for Papers
  October 2-4, 1998, Amsterdam
* Topics.  Suggested, but not exclusive topics of interest for the
  workshop are: combination of constraint solving techniques and
  combination of decision procedures; integration of equational and
  other theories into deductive systems; integration of data
  structures into CLP formalisms and deduction processes; combinations
  of logics and of term rewriting systems; hybrid systems in
  computational linguistics, knowledge representation, natural
  language processing, and human computer interaction; logical
  modeling of multi-agent systems.
* Program committee.  Franz Baader, David Basin, Jacques Calmet, Dov
  Gabbay (co-chair), Natasha Kurtonina, Aart Middeldorp, Istvan
  Nemeti, Maarten de Rijke (co-chair), Christophe Ringeissen, Klaus
  Schulz, Amilcar Sernadas, Michael Wooldridge
* Paper submissions.  Authors are invited to submit a detailed
  abstract of a full paper of at most 10 pages to the second programme
  co-chair, either by e-mail (preferred) or regular mail.  Results
  must be unpublished, and not submitted for publication elsewhere.
  The cover page should include title, authors, and the coordinates of
  the corresponding author.  Following this it should be indicated
  which of the thematic areas best describes the content of the paper.
  To be considered, submissions must be received no later than May 15,
  1998.  Electronic submissions should be sent to, using `Submission' as the subject line.

  Call For Papers
  Pisa, Italy, 14--18 September 1998
* Scope of SAS'98.  Contributions are welcome on all aspects of Static
  Analysis, including, but not limited to Abstract Interpretation,
  Data Flow Analysis, Complexity, Theoretical Frameworks, Experimental
  Evaluation, Verification Systems, Specific Analyses, Type Inference,
  Partial Evaluation, Optimising Compilers, Abstract Domains.
* Scope of PLILP/ALP'98 Topics of interest include, but are not
  limited to Functional, Logic, and Constraint Programming,
  Object-Oriented Programming, Integration of Different Paradigms,
  Concurrent Extensions, Typing and Structuring Systems, Executable
  Specifications, Implementation of Declarative Languages, Compiler
  Specification and Construction, Parallel and Distributed
  Implementations, Programming Environments.
* SAS Program Chair. Giorgio Levi (Pisa, Italy). 
* PLILP/ALP Program Chair. Catuscia Palamidessi (Penn State, USA). 
* Paper submissions.  The submission deadline is April 3, 1998.
  Papers must describe original, previously unpublished work, and must
  not be simultaneously submitted for publication elsewhere.  They must
  be written in English, must not exceed 15 pages (Springer LNCS
  format, excluding references and figures), and must contain a cover
  page containing the following: a 200-word abstract, keywords, postal
  and electronic mailing addresses, and phone and fax numbers of one
  of the authors.  Submission is electronic (up to exceptions):
  submission guidelines will appear on the web site given under
  Additional Information.

  Call for Papers
  June 18th 1998, Marstrand, Sweden
  In Conjunction with Mathematics of Program Construction Conference
* The goal of the workshop is to inventory the full diversity of
  research activities in the area of generic programming, both
  theoretical and applied, by attracting as wide a spectrum of
  participants as possible to the workshop.  The results of the
  workshop will be published in the form of a detailed summary of all
  presentations, prepared by the organizers and made available on
* We cordially invite all those with an active interest in this
  important new  area to submit a short position paper on their work
  to Roland Backhouse (  The position paper should
  outline your current research activities in this area and include
  references to published papers and/or  web links to technical
  reports where more information can be found.   The recommended
  length is approximately three pages.  The deadline for submission is
  16th February, 1998.    
* Organizers.  Roland Backhouse (Cochair), Tim Sheard (Cochair), Robin
  Cockett, Barry Jay, Johan Jeuring, Karl Lieberherr, Oege de Moor,
  Bernhard Moeller, Jose Oliveira, Fritz Ruehr.