AARNEWS - March 2004



No. 62, March 2004

From the AAR President
Workshops Associated with IJCAR - Call for Papers

  • Empirically Successful First Order Reasoning
  • UNIF 2004
  • Workshop on Disproving - Nontheorems, Nonvalidity, Nonprovability

  • Thesis Abstracts
  • Korovin thesis: Knuth-Bendix Orders in Automated Deduction and Term Rewriting
  • Pientka thesis: Tabled Higher-Order Logic Programming

  • Call for Papers
  • MKM 2004
  • CSL 04
  • AIML'2004
  • JELIA'04

  • Senior Research Positions in Logic and Computation

    From the AAR President, Larry Wos...

    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.

    Workshops Associated with IJCAR - Call for Papers

    Empirically Successful First Order Reasoning

    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.


  • Implementation techniques and comparisons
  • Data structures and algorithms for the efficient representation of terms, formulas, search states, and so forth
  • Higher-level data structures and formats for the representation of proof tasks and derivations, proof and lemma storage, and so forth
  • Implemented and evaluated heuristics
  • Applications

  • Descriptions of automated reasoning solutions in applications domains
  • Experiences with practical applications
  • Encoding of domain problems into logic, and decoding of logic solutions in to the domain
  • Special automated reasoning techniques for applications
  • User interfaces (to whole systems, not just the automated reasoning component)
  • System integration
  • The deadline for submission is April 11, 2004. Submissions must be emailed to Geoff Sutcliffe ( geoff@cs.miami.edu). Authors of selected papers will be invited to submit an extended paper for the International Journal of Artificial Intelligence Tools, scheduled to appear in June 2005.

    Also invited are proposals for system and application demonstrations. Full details are available on the Web.


    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:


    Definition, design, implementation and application:

    Specialization and integration:

    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.

    For further information see the Web site.

    UNIF 2004

    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:


    Related Topics


    Authors are invited to submit via e-mail an abstract (1-5 pages), a paper (no longer than 15 pages), or a system description (no more than 5 pages) in Postscript or PDF format to unif04@iu-bremen.de before May 14, 2004. The deadline for electronic submission is Friday, May 14, 2004. Accepted papers, abstracts and system descriptions will be included in the proceedings which will be available at the workshop. For further information, see the Web site.

    Workshop on Disproving - Nontheorems, Nonvalidity, Nonprovability

    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.

    The submission deadline is April 18, 2004. For details, please see the workshop Web page.

    Thesis Abstracts

    Title of Thesis 1:

    Knuth-Bendix Orders in Automated Deduction and Term Rewriting

    Author: Konstantin Korovin

    Institution: The University of Manchester (UK)

    Supervisor: Prof. Andrei Voronkov

    Exam date: November 2003


    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.

    Title of Thesis 2:

    Tabled Higher-Order Logic Programming

    Author: Brigitte Pientka

    Institution: Carnegie Mellon University

    Supervisor: Frank Pfenning

    Web page: http://www.cs.mcgill.ca/~bientka/

    Abstract: Note: This thesis was published as a technical report, CMU-CS-03-185, December 2003.

    A logical framework is a general meta-language for specifying and implementing deductive systems, given by axioms and inference rules. Based on a higher-order logic programming interpretation, it supports executing logical systems and reasoning with and about them, thereby reducing the effort required for each particular logical system. In this thesis, we describe different techniques to improve the overall performance and the expressive power of higher-order logic programming. First, we introduce tabled higher-order logic programming, a novel execution model where some redundant information is eliminated using selective memoization. This extends tabled computation to the higher-order setting and forms the basis of the tabled higher-order logic programming interpreter. Second, we present efficient data-structures and algorithms for higher-order proof search. In particular, we describe a higher-order assignment algorithm that eliminates many unnecessary occurs checks and develop higher-order term indexing. These optimizations are crucial to make tabled higher-order logic programming successful in practice. Finally, we use tabled proof search in the meta-theorem prover to reason efficiently with and about deductive systems. It takes full advantage of higher-order assignment and higher-order term indexing.

    As experimental results demonstrate, these optimizations taken together constitute a significant step toward exploring the full potential of logical frameworks in practice.

    Call for Papers

    MKM 2004

    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

    Papers should be sent to the program committee at mkm2004submission@mizar.uwb.edu.pl. The deadline for submissions is April 15, 2004. Accepted papers will appear in the proceedings before the conference, published in the Springer-Verlag Lecture Notes in Computer Science series. Submitted papers must be prepared according to Authors Instructions of LNCS. Authors of accepted papers are expected to present their work at the conference.

    For further information, see the Web site.

    CSL 04

    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.

    For further information, see the Web site.


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

    Authors are invited to submit a detailed abstract of a full paper of at most 10 pages. Submissions are due April 15, 2004. For further details see the Web site.

    Preliminary versions of the full papers will be made available at the meeting. Authors will be invited to submit a full version, which will again be refereed. The selected papers will be included in the formal proceedings to be published by King's College Publications.


    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:

    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.

    For further details see the Web site.

    Senior Research Positions in Logic and Computation

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

    For information about NICTA and the program, and details of how to apply, see the Web site (follow the "Positions Vacant" link).

    The closing date for applications is April 16, 2004.

    Gail W. Pieper
    Technical editor
    March 2004