NEWSLETTER No. 80, March 2008

From the AAR President
ProofBuilder: A Versatile Interactive Prover for Beginning Students

  • Workshop on Automated Reasoning
  • PAAR-2008
  • VERIFY 2008
  • CEDAR'08
  • Annals of Mathematics and Artificial Intelligence
    Call for Papers for Conferences
  • JELIA 2008
  • RTA 2008
  • MICAI 2008
  • IMLA'08
  • AiML-2008
  • Computational Logic and Cognitive Science

    From the AAR President, Larry Wos...
    If I were a traveling man, I would say this summer would be an ideal time to travel the world -- from Pennsylvania to Austria to Australia -- participating in several exciting conferences and workshops on automated reasoning. I am particularly intrigued by the new workshop titled PAAR, which appears to emphasize the application of reasoning programs to real problems. While I am interested in theory, the way one can truly measure the success of automated reasoning is in the number, variety, and type of problem that can be solved.

    Since I am not a traveling man but have, like most of the world, gotten involved with the Internet, I recently noted that the Wikipedia article on automated reasoning could use an update. Certainly, I do not consider the area a "subfield of artificial intelligence" -- though perhaps AAR readers do, in which case we could launch an interesting debate.

    ProofBuilder: A Versatile Interactive Prover for Beginning Students

    ProofBuilder runs straightforwardly on all platforms with Java; it allows users to copy/paste formulas from Web pages, MS Word, PDF, and so forth; it adapts to the symbols that users enter for "implies," "forall," and the like; and it supports many proof styles including transforming expressions according to logical equivalences or equations or comparisons ("<", ">", etc.), direct proof, backward chaining, handling subcases separately, nonclausal resolution, proof by example or counterexample, stepwise and strong induction, and proof by contradiction.

    This prover can handle the material of an introductory course or textbook on Discrete Mathematics, including propositions, quantifiers, sets, summations, O(), divisors, modulus, and combinatorics.

    The author of ProofBuilder is Hugh McGuire, from Grand Valley State University, MI, U.S.A. For further information, see the documentation with examples on the Web.


    Workshop on Automated Reasoning

    ARW will take place July 30-31, 2008, at the University of Birmingham. Titled "Bridging the Gap between Theory and Practice," this workshop continues the series workshops and will provide an informal forum for the automated reasoning community to discuss recent work, new ideas and current trends. It aims to bring together researchers from all areas of automated reasoning in order to foster links and facilitate cross-fertilization of ideas among researchers from various disciplines; among researchers from academia, industry and government; and between theoreticians and practitioners.

    The series covers the full breadth and diversity of automated reasoning, including topics such as logic and functional programming; equational reasoning; deductive databases; unification and constraint solving; the application of formal methods to specifying, deriving, transforming and verifying computer systems and requirements; deductive and non-deductive reasoning, including abduction, induction, nonmonotonic reasoning, and analogical reasoning; commonsense reasoning; and the wide range of topics that fall under the heading of knowledge representation and reasoning.

    The workshops in this series are highly interactive, giving all attendees the opportunity to participate. The workshops contain many open discussion sessions organized around specific topics, and often contain sessions for displaying posters and presenting system demonstrations. This is intended to be an inclusive workshop, with participants encouraged from the broad spectrum covered by the field of automated reasoning. We encourage the participation of experienced researchers as well as those new to the field, especially students.

    For more details see the ARW 2008 Web site.


    The first workshop on Practical Aspects of Automated Reasoning will be held August 10 or 11, 2008, in Sydney, Australia. PAAR will be associated with the 4th International Joint Conference on Automated Reasoning (IJCAR-2008).

    PAAR provides a forum for developers of automated reasoning tools to discuss and compare different implementation techniques, and for users to discuss and communicate their applications and requirements. This workshop will bring together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools. It will allow researchers to present their work in progress, and to discuss new implementation techniques and applications.

    Topics include the following:

  • automated reasoning in classical and nonclassical logics, implementation of provers;
  • automated reasoning tools for all kinds of practical problems and applications;
  • practical experiences, case studies, feasibility studies;
  • evaluation of implementation techniques and automated reasoning tools;
  • benchmarking approaches;
  • nonstandard approaches to automated reasoning, nonstandard forms of automated reasoning, new applications;
  • implementation techniques, optimization techniques, strategies and heuristics;
  • system descriptions and demos.
  • We are particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems in practice, and how to apply existing systems to real problems.

    Researchers interested in participating are invited to submit a short (2-10 pages) abstract via EasyChair. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions.

    Submissions should be in standard-conforming Postscript or PDF. To submit a paper, go to the EasyChair PAAR page and follow the instructions there. The final versions should be prepared in LaTeX using the Springer Verlag llncs class. The workshop proceedings will be published as a technical report and distributed at the event.

    If quality and quantity of the subissions warrants this, we plan to produce a special issue of a recognized journal on the topic of the workshop.

    Abstracts are due May 27, 2008; camera-ready versions due: July 7th, 2008 For further information, please see the Web site.

    VERIFY 2008

    The 5th International Verification Workshop (VERIFY 2008) will be held in Sydney, Australia, August 10-11.

    The VERIFY workshop series brings together people interested in the development of safety and security critical systems, in formal methods, in the development of automated theorem proving techniques, and in the development of tool support. Practical experiences gained in realistic verifications are of interest to the automated theorem proving community and new theorem-proving techniques should be transferred into practice. The overall objective of the VERIFY workshops is to identify open problems and to discuss possible solutions under the theme What are the verification problems? and What are the deduction techniques?

    The scope of VERIFY includes topics such as the following:

  • ATP techniques in verification
  • Case studies (specification and verification)
  • Combination of verification tools
  • Integration of ATPs and CASE-tools
  • Compositional and modular reasoning
  • Experience reports on using verification
  • Gaps between problems and techniques
  • Formal methods for fault tolerance
  • Abstracts are due May 14, and paper submissions May 22.


    The goal of CEDAR is to bring together researchers interested in problems that are in the interface between automated reasoning and computational complexity, in particular in the following:

  • identifying (fragments of) logical theories which are decidable, identifying fragments thereof which have low complexity, and analyzing possibilities of obtaining optimal complexity results with uniform tools;
  • analyzing decidability in combinations of theories and possibilities of combining decision procedures;
  • efficient implementations for decidable fragments;
  • application domains where decidability resp. tractability are crucial.
  • Topics of interest for CEDAR 2008 include the following:

  • Complexity: complexity analysis for fragments of first- (or higher) order logic and complexity analysis for combinations of logical theories
  • Expressibility (in logic, automated reasoning, algebra) Application domains for which complexity issues are essential (verification, security, databases, ontologies)
  • We plan to accept three types of papers:

  • Original papers (up to 15 pages, LNCS style, including bibliography); should describe original research and contain sufficient detail to assess the merits and relevance of the contribution. Simultaneous submission of material is prohibited.
  • Work in progress (up to 6 pages, LNCS style, without bibliography).
  • Presentation-only papers (please submit an abstract of up to 3 pages, LNCS style + a link to the already published paper): may describe work previously published. The abstracts of accepted presentation-only papers will appear in the informal proceedings to be distributed at the workshop (full papers in this category will not be inserted in the proceedings).
  • We are allowing the submission of previously published work in order to allow researchers to communicate good ideas that the attendees may not be aware of.

    Given the informal style of the workshop, the submission of papers presenting student's work and work in progress is encouraged. Submission of papers is via Easychair.

    The final versions of the selected contributions will be collected in a volume to be distributed at the workshop. These informal proceedings will also be made accessible on the web. A special journal issue is planned.

    For further information, see the Web site.

    Annals of Mathematics and Artificial Intelligence
    Special Issue on First-Order Theorem Proving
    Guest Editors: Silvio Ranise and Ullrich Hustadt

    First-order theorem proving is one of the core themes of automated deduction and one of its most mature subfields. First-order logic is sufficiently expressive to allow the specification of a wide range of problems in a natural way. At the same time an extensive variety of sound and complete calculi for first-order logic exists which have been implemented in a number of high-quality, fully automated reasoning systems. These in turn make it not only possible to effectively solve problems formulated in first-order logic, but also make it attractive to consider closely related logics, for example, many-valued, description, and modal logics, from a first-order perspective.

    This special issue is intended to present recent advances in the field to an audience of applied logicians, automated deduction theorists and applications specialists.

    This special issue will focus on first-order theorem proving as a core theme of automated deduction, in particular:

  • theorem proving in first-order classical, many-valued, description, and modal logics, including constraint reasoning, decision procedures, equational reasoning, model construction, paramodulation/superposition, resolution, satisfiability modulo theories, tableaux, term rewriting, unification;
  • strategies and complexity of theorem proving procedures;
  • applications of first-order theorem proving to program verification, model checking, artificial intelligence, mathematics, computational linguistics.
  • This special issue welcomes original high-quality contributions that have been neither published in nor submitted to any journals or refereed conferences. Authors of papers presented at
    FTP 2007 are welcome to submit extended and revised versions of their papers. However, contributions are not limited to those based on papers presented at FTP 2007; other submission are welcome as well.

    The deadline for submissions is May 28, 2008. For further details see the Web page.

    Call for Papers for Conferences

    JELIA 2008

    The 11th European Conference on Logics in Artificial Intelligence will take place September 28 to October 1, 2008, in Dresden, Germany. JELIA 2008 strives to foster links and facilitate cross-fertilization of ideas between researchers from various disciplines, between researchers from academia and industry, and between theoreticians and practitioners. Authors are invited to submit papers presenting original and unpublished research in all areas related to the use of logics in AI. Topics of interest include the following:

  • Reasoning including deduction, abduction and induction
  • Nonmonotonic, uncertain, probabilistic reasoning
  • Reasoning about situations, actions, and causality
  • Belief change, including revision, update, and merging
  • Knowledge representation and reasoning
  • Classical as well as non-classical logics, including modal, temporal, and spatial logics
  • Fuzzy logic
  • Description logics
  • Logic-based ontology languages
  • Theorem proving
  • Logic and constraint programming
  • Answer set programming
  • Computational complexity and expressiveness of logic-based systems
  • Logic-based applications to the Semantic Web
  • Logic-based planning and diagnosis
  • Logics and multiagent systems
  • Logics in machine learning
  • The deadline for submission is June 2, 2008. Proceedings will be published by Springer-Verlag in the Lecture Notes on Artificial Intelligence series.

    Further information about JELIA 2008 is available at the Web site.

    Rewriting Techniques and Applications

    The 19th International Conference on Rewriting Techniques and Applications (RTA 2008) will be held on July 15-17, 2008, at the Castle of Hagenberg, Austria. The conference is organized as part of the RISC Summer 2008, which comprises five conferences, five workshops and the Training School in Symbolic Computation, and is followed by the 3rd International School on Rewriting in Obergurgl.

    RTA is the major forum for the presentation of research on all aspects of rewriting. Typical areas of interest include the following:

  • Applications: case studies; analysis of cryptographic protocols; rule-based (functional and logic) programming; symbolic and algebraic computation; theorem proving; system synthesis and verification; proof checking; reasoning about programming languages and logics; program transformation
  • Foundations: matching and unification; narrowing; completion techniques; strategies; rewriting calculi, constraint solving; tree automata; termination; combination
  • Frameworks: string, term, and graph rewriting; lambda-calculus and higher-order rewriting; constrained rewriting/deduction; categorical and infinitary rewriting; integration of decision procedures
  • Implementation: implementation techniques; parallel execution; rewrite tools; termination checking;
  • Semantics: equational logic; rewriting logic; rewriting models of programs.
  • Submission categories include regular research papers (15 pages) and system descriptions (10 pages). Problem sets and submissions describing interesting applications of rewriting techniques are also welcome. Papers must be submitted electronically through the EasyChair system,

    An award will be given to the best paper or papers as decided by the program committee.

    Limited student support will be available and announced in future versions of this call.

    For further information, see the Web page.

    MICAI 2008

    The 7th Mexican International Conference on Artificial Intelligence will take place in Mexico City, Mexico, October 27-31, 2008. Topics of interest include all areas of artificial intelligence. Poster session, workshops, tutorials, and cultural events are planned. Papers accepted for oral session will be published by Springer in LNAI: Lecture Notes in Artificial Intelligence. Poster session papers will be published separately. Special issues of journals are anticipated. Submissions are received via the Web. Abstracts are due May 5, full text by May 12. General inquiries should be sent to micai2008 at


    The Fourth International Workshop on Intuitionistic Modal Logic and Applications (IMLA'08) will take place in Pittsburgh, Pennsylvania, June 23, 2008. Constructive modal logics and type theories are of increasing foundational and practical relevance in computer science. Applications are in type disciplines for programming languages, and meta-logics for reasoning about a variety of computational phenomena. Theoretical and methodological issues center around the question of how the proof-theoretic strengths of constructive logics can best be combined with the model-theoretic strengths of modal logics. Practical issues center around the question which modal connectives with associated laws or proof rules capture computational phenomena accurately and at the right level of abstraction. This workshop will bring together designers, implementers, and users to discuss all aspects of intuitionistic modal logics and type theories. Topics include the following:

  • applications of intuitionistic necessity and possibility
  • monads and strong monads
  • constructive belief logics and type theories
  • applications of constructive modal logic and modal type theory to formal verification, foundations of security, abstract interpretation, and program analysis and optimization
  • modal types for integration of inductive and co-inductive types, higher-order abstract syntax, strong functional programming
  • models of constructive modal logics such as algebraic, categorical, Kripke, topological, and realizability interpretations
  • notions of proof for constructive modal logics
  • extraction of constraints or programs from modal proofs
  • proof search methods for constructive modal logics and their implementations
  • We solicit submissions on work in progress and on more mature results. Submissions should be extended abstracts of 5-10 pages sent in PostScript or PDF format to the program co-chair at Submissions are due April 25, 2008. We plan to publish the workshop proceedings as Electronic Notes in Theoretical Computer Science (ENTCS) or in CEURS, to be decided. Authors should use the generic ENTCS macro package.

    For further information, see the Web page.


    Advances in Modal Logic will take place at LORIA in Nancy, France, September 9-12, 2008.

    AiML is an initiative aimed at presenting an up-to-date picture of 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.

    Authors are invited to submit on all aspects of modal logics, including the following:

  • history of modal logic
  • philosophy of modal logic
  • applications of modal logic
  • computational aspects of modal logic
  • theoretical aspects of modal logic
  • specific instances and variations of modal logic
  • In a change from previous AiML's, there will be two types of paper: full papers for publication and presentation at the conference, and abstracts for short presentation only. Both types of paper should be submitted electronically using the submission page. The online submission system will be opened a few weeks before the submission deadline of March 31, 2008.

    Full papers (max. 15 pages) will be published by College Publications in a volume to be made available at the meeting. Abstracts should at most 5 pages. They may describe preliminary results, work in progress, and so forth and will be subject to light review. They may be made available at the conference, and authors should indicate if they would like to make a short presentation of their abstract of up to 15 minutes.

    Computational Logic and Cognitive Science
    Technische Universitaet Dresden
    August 24 - September 6, 2008

    The summer academy at TU Dresden will focus on the long-lasting controversy of the relationship between modern formal logic (including its use for automated reasoning and computation) and the rationality and common sense underlying human reasoning. Traditionally, a huge gap is perceived between the symbolic representation of knowledge used in modern logic and the subsymbolic representation considered dominant in human reasoning. Psychological experiments even suggested that people often don't reason logically and, in general, that logic seems to play only a minor role in human reasoning. However, recently, new ways of explaining human reasoning seem to revive its relatedness to logic. For this reason this summer academy seeks to bring together researchers from both sides for an exchange of views.

    The participation fee is 200 EUR. A limited number of grants may be available. Applicants should indicate in the application if a grant is essential for participation. Applications for grants must include an estimate of travel costs (to be filled in the respective part of the online registration form).

    Participants must register by April 1, 2008 (see the online registration on the Web page). For those who want to apply for a grant, this deadline is obligatory. After April 1, 2008, registration will be possible as long as there are vacant places. People applying until April 1, 2008, and applying for a grant will be informed about respective decisions on grants at the latest by the end of April.

    It will be possible for some participants to present their research work during a small workshop integrated in the summer school. Those wishing to do so should register by means of the online workshop registration form on the web page (the title of the proposed talk, and, in addition, an extended abstract or a full paper of at most 10 pages in postscript or pdf format must be submitted by April 1, 2008). Participation at the summer school is a prerequisite for participation at the workshop.

    The course program is as follows:

  • COMPUTATIONAL LOGIC AND COGNITIVE SCIENCE: AN OVERVIEW -- Kai-Uwe Kuehnberger, Helmar Gust (Universitaet Osnabrueck)
  • HUMAN REASONING AND COGNITIVE SCIENCE -- Michiel van Lambalgen (University of Amsterdam, The Netherlands) and Keith Stenning (Edinburgh University, UK)
  • COMPUTATIONAL LOGIC AND CONNECTIONIST SYSTEMS -- Steffen Holldobler (Technische Universiaet Dresden)
  • COMPUTATIONAL LOGIC IN HUMAN REASONING -- Robert Kowalski (Imperial College, Department of Computing, UK)
  • LOGIC-BASED AGENTS -- Fariba Sadri (Imperial College, Department of Computing, UK)
  • THE LOGIC OF GENERALIZED TRUTH VALUES: A TOUR INTO PHILOSOPHICAL LOGIC -- Heinrich Wansing (Fakultaet fuer Philosophie, Technische Universitaet Dresden)
  • COMPUTATIONAL LOGIC APPLICATIONS IN COGNITIVE SCIENCES -- Luis Moniz Pereira (Universidade Nova de Lisboa, Portugal)