[Past issues of the newsletter are available at http://www.bell-labs.com/topic/conferences/lics/ BOOK ANNOUNCEMENT 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: 70544.2431@Compuserve.com. MATHEMATICAL FOUNDATIONS OF PROGRAMMING SEMANTICS (MFPS 14) 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 mfps@math.tulane.edu 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. SPECIAL ISSUE OF THE JOURNAL OF SYMBOLIC COMPUTATION 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 (bonacina@cs.uiowa.edu) and Ulrich Furbach (uli@mailhost.uni-koblenz.de). THE FIRST INTERNATIONAL WORKSHOP ON LABELED DEDUCTION (LD'98) 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 ld98@informatik.uni-freiburg.de, before April 15, 1998. * Organizing Committee. David Basin and Luca Vigano. * Program Committee. David Basin, Marcello D'Agostino, Dov Gabbay, Sean Matthews, Luca Vigano`. FORMAL METHODS IN SYSTEM DESIGN 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: http:www.wkap.nl. 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, email: jkemp@wkap.com. 9th INTERNATIONAL CONFERENCE ON CONCURRENCY THEORY (CONCUR'98) Call for papers Nice, France, September 8-11, 1998 concur98@sophia.inria.fr * 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 c98-subm@sophia.inria.fr. 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. 8th INTERNATIONAL WORKSHOP ON LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION Call for papers Manchester, United Kingdom, 15 - 19 June 1998 http://www.cs.man.ac.uk/~kung-kiu/lopstr98 * 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. APPLICATIONS OF TREE AUTOMATA IN REWRITING, LOGIC AND PROGRAMMING 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. WORKSHOP ON CONSTRAINT DATABASES (CDB'98) 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 cdb98@wiwi.hu-berlin.de. 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 POSITION AVAILABLE 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: baader@informatik.rwth-aachen.de, phone: (++49 241)-8021131, fax: (++49 241)-8888360. CATEGORICAL REWRITING 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 http://www.etl.go.jp/~ferjan/CatTRS.html. * Organizers. Neil Ghani, Christoph Lueth, Fer-Jan de Vries. BRITISH COLLOQUIUM FOR THEORETICAL COMPUTER SCIENCE (BCTCS 14) 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. 2nd WORKSHOP ON FRONTIERS OF COMBINING SYSTEMS (FroCoS'98) 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 frocos98@wins.uva.nl, using `Submission' as the subject line. JOINT INTERNATIONAL SYMPOSIA SAS'98 AND PLILP/ALP'98 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. WORKSHOP ON GENERIC PROGRAMMING 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 internet. * 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 (rolandb@win.tue.nl). 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.