IJCAR is a comin' in, and this issue of the AAR Newsletter includes calls for three exciting workshops to be held in conjunction with IJCAR. Those who know me will not be surprised that I have put the workshop on strategies first. I have long believed that strategies are the key to powerful automated reasoning programs. But I also confess that my interest was piqued by the other two workshops also: the topic of ``disproving'' is a fine complement to proof finding; and the aim of UNIF 2004 to present ``even unfinished'' work will, I hope, encourage fruitful discussion about unification.

The IJCAR 2004 Workshop on Empirically Successful First Order Reasoning (ESFOR) will bring together practioners and researchers who are concerned with the implementation and deployment of working automated reasoning systems for first-order logic. The workshop will discuss "really running" systems, and not theoretical ideas that have not yet been translated into working systems.

Authors are invited to submit papers (of up to 20 pages) in one of the following topic areas.

Systems

Applications

The 5th International Workshop on Strategies in Automated Deduction will be held at Cork, Ireland, July 4, 2004. The workshop is the primary forum for the communication of new results on control strategies and search plans in automated theorem proving, automated model building, decision procedures, interactive proof assistants, proof planners, and logical frameworks, in first-order (including propositional and purely equational as special cases), modal (e.g., temporal) and higher-order logics.

Topics of interest include the following:

Theory:

• Models of search spaces and languages or mathematical formalisms to define strategies and prove properties about them, including machine-independent evaluation and comparison of strategies
• Analysis of the search space (e.g., regularities, symmetries, classification, stratification)
• Strategy analysis (e.g., formal approaches for the machine-independent evaluation and comparison of deduction strategies)

Definition, design, implementation and application:

• Metalevel features (e.g., pre-processing, compilation, lemmatization, caching, usage of semantics or domain knowledge)
• Strategies in (existing) systems (e.g., implementation of the proof search model, flexibility and programmability of strategies, role of the user)
• Applications and case studies in which strategies play a major role

Specialization and integration:

• Strategies devoted to specific theories including inductive theories, arithmetic, decidable theories, and combinations of theories
• Control issues and strategies in the integration of systems

Researchers are invited to submit an extended abstract of up to 10 pages or to send a position paper of 1-2 pages. Authors of accepted extended abstracts will be invited to present their work at the workshop. Authors of position papers will be invited to participate, and may be invited to give shorter talks if time allows it. All submissions should be sent to the program chairs (strategies04@imag.fr) in Postscript before April 19, 2004. Accepted contributions will be included in the workshop proceedings, which will be available at the workshop and on the Web.

Based on the submissions, the program chairs will consider the possibility of a post-workshop publication (e.g., a special issue of a journal or a volume in a series of electronic proceedings), where authors may submit full versions of the workshop papers. This may involve another call for papers and refereeing process.

The 18th International Workshop on Unification will be held July 4-5, 2004, at Cork, Ireland. UNIF is the main international meeting on unification. Unification is concerned with the problem of identifying given terms, either syntactically or modulo a given logical theory. Syntactic unification is the basic operation of most automated reasoning systems, and unification modulo theories can be used, for instance, to build in special equational theories into theorem provers.

The aim of UNIF 2004 is to to bring together people interested in unification, present recent (even unfinished) work, and discuss new ideas and trends in unification and related fields. In particular, it offers a good opportunity for young researchers and researchers working in related areas to get an overview of the state of the art in unification theory and to meet with the experts in the field.

Topics of interest include the following:

Unification

• E-unification
• Unification algorithms
• Higher-order unification
• String unification
• Context unification
• Combination problems
• Disunification
• Typed unification

Related Topics

• Constraint solving
• Tree descriptions
• Matching
• Narrowing

Applications

• Type checking and type inference
• Automated deduction
• Rewriting
• Functional and logic programming
• Grammars
• Computational linguistics
• Implementations

A workshop on disproving will be held at Cork, Ireland, July 4, 2004. The workshop aims at identifying nontheorems, that is, showing nonvalidity, and providing some kind of proof of nonvalidity. The scope of the workshop covers every method that is able to discover nontheorems and, ideally, explain why the formula is not a theorem. Possible subjects are decision procedures, model generation methods, reduction to SAT, formula simplification methods, abstraction-based methods, and failed-proof analysis.

Title of Thesis 1:

Author: Konstantin Korovin

Institution: The University of Manchester (UK)

Supervisor: Prof. Andrei Voronkov

Exam date: November 2003

Abstract:

Ordering restrictions play a crucial role in automated deduction. In particular, orders are used extensively for pruning search space in automated theorem provers and for rewriting-based reasoning and computation. There are two classes of orders that are widely used in automated deduction: Knuth-Bendix orders and various versions of recursive path orders. Despite the fact that Knuth-Bendix orders were discovered earlier than recursive path orders, and since then have been used in many state-of-the-art automated theorem provers, the decidability and complexity of many important problems related to these orders remained open.

In this thesis we try to close this gap and provide various decidability and complexity results for a number of important decision problems related to Knuth-Bendix orders. We prove the decidability and NP-completeness of the problem of solving Knuth-Bendix ordering constraints. n the case of constraints consisting of single inequalities we present a polynomial-time algorithm. We also prove the decidability of the problem of solving general first-order Knuth-Bendix ordering constraints over unary signatures. Another problem we study is the orientability problem by Knuth-Bendix orders. We present a polynomial-time algorithm for orientability of systems consisting of term rewrite rules and equalities by Knuth-Bendix orders, and prove that this problem is P-complete. Finally, we show that it is possible to extend Knuth-Bendix orders to AC-compatible orders preserving attractive properties of Knuth-Bendix orders.

Author: Brigitte Pientka

Institution: Carnegie Mellon University

Supervisor: Frank Pfenning

The Third International Conference on Mathematical Knowledge Management will take place September 19-21, 2004, in Bialowieza, Poland.

Mathematical knowledge management is a new field in the intersection of mathematics and computer science. It is motivated by the need for new techniques to manage the enormous volume of mathematical knowledge available in current mathematical sources and making it available through the new developments in information technology.

Mathematical knowledge is a treasure unsurpassed in its extent, richness, and interconnectedness, its vitality to engineering, science, and mathematics itself, its daily use by millions of people. Thus, mathematical knowledge seems to be an excellent candidate for testing innovative theoretical and technological solutions for content-based information systems, their interoperability, and management of machine processable information on the Semantic Web.

The conference aims to bring together mathematicians, software developers, publishing companies, mathematics organizations, and teachers for exchanging their views and approaches, current activities and new initiatives. We are seeking original contributions to theoretical, technological, and pragmatical aspects of mathematical knowledge management. Papers focused on system or projects descriptions and comparison, standardization efforts, critical surveys, large experiments, and case studies are particularly welcome. Of particular interest are the following:

Authoring languages and tools	MathML- and XML-based standards
Computer algebra systems	Metadata
Datamining	Deduction systems
Digital libraries	Math assistants
Interactive learning	Searching and retrieving
Web presentation of mathematics	Languages of mathematics
Knowledge representation	Repositories of formalized mathematics

The 13th Annual Conference of the European Association for Computer Science Logic will take place in Karpacz, Poland, September 20-24, 2004.

The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. The proceedings will be published in the Springer Lecture Notes in Computer Science. Papers accepted by the program committee must be presented at the conference by one of the authors. Submitted papers must describe work not previously published. They must not be submitted concurrently to another conference with refereed proceedings. Research that is already submitted to a journal may be submitted to CSL, provided that the program chair is notified in advance that this is the case and that the paper is not scheduled forjournal publication before the conference.

The submission deadline is in two stages: abstracts are due April 3, 2004; full papers are due April 10, 2004.

The Advances in Modal Logic conference will be held in Manchester, UK, September 9-11, 2004. AIML is an initiative aimed at presenting the state of the art in modal logic and its many applications. The initiative consists of a conference series together with volumes based on the conferences.

AiML-2004 is the fifth conference organized as part of this initiative. The conference will include a special session ``Modal Logics for Knowledge and Action.'' Invited speakers include Philippe Balbiani (Toulouse), Keith Devlin (Stanford) , Valentin Goranko (Johannesburg), Wiebe van der Hoek (Liverpool), Maarten Marx (Amsterdam), and Robert Stalnaker (MIT).

The European Conference on Logics in Artificial Intelligence will take place in Lisbon, Portugal, September 27-30, 2004. The aim of JELIA'04 is to bring together active researchers interested in the use of logics in artificial intelligence. Discussions will focus on current research, results, problems, and applications--both theoretical and practical. Topics of interest include the following:

• Abductive and inductive reasoning
• Applications of logic-based systems
• Automated reasoning and theorem proving
• Computational complexity and exprressiveness in AI
• Description logics
• Foundations of logic programming and knowledge-based systems
• Logic-gased AI systems
• Logic-based applications to the Semantic Web
• Nonmonotonic reasonoing
• Uncertain and probabilistic reasoning

Abstracts must be submitted by May 6, and full papers by May 9. Accepted papers will be published by Springer-Verlag as a volume of the Lecture Notes on Artificial Intelligence series.

The Logic and Computation Program at National ICT Australia (NICTA) invites applications for two continuing positions at the senior researcher level or above. Experienced researchers with expertise in pure and applied logic, mechanized reasoning, or the logical foundations of computation who may be interested in joining this new research center and helping to shape the Logic and Computation Program should contact the program leader (John.Slaney@nicta.com.au).