No. 68 October 2005

From the AAR President, Larry Wos... Education is key, we are told, to keeping our society strong and flourishing. I am delighted, therefore, to see that several people have recently received doctoral degrees in automated reasoning. I hope they will in turn become guiding lights for the next generation of researchers!

On a different note, let me point our readers to the call for papers for a special issue of the Journal of Automated Reasoning. Most attractive, to me, is the emphasis being placed on ``really working'' systems and applications. While theory is certainly important, I have--throughout my career--stressed the value of translating ideas into working software and then testing those ideas on real applications.

Announcement of CADE Elections
Amy Felty
(Secretary of AAR and CADE)

An election of CADE trustees will be held soon, and all AAR members will receive a ballot. The following people are currently serving as trustees of CADE Inc.:

Franz Baader (President, CADE-19 Program Chair, elected 10/2003)
David Basin (IJCAR 2004 Program Co-chair, elected 10/2004)
Peter Baumgartner (elected 10/2003)
Maria Paola Bonacina (Secretary 9/1999 to 5/2004, elected 10/2004)
Amy Felty (Secretary, appointed 5/2004)
Uli Furbach (IJCAR 2006 co-Program Chair)
Rajeev Goré (elected 10/2004)
Michael Kohlhase (elected 10/2000, reelected 10/2003)
Neil Murray (Treasurer)
Robert Nieuwenhuis (CADE-20 Program Chair: term expiring)
Geoff Sutcliffe (elected 10/2004)
Andrei Voronkov (Vice President, CADE-18 Program Chair (elected 10/2002: term expiring)
Toby Walsh (elected 10/2002: term expired)

The terms of Robert Nieuwenhuis, Andrei Voronkov, and Toby Walsh are expiring. The position of Robert Nieuwenhuis will be taken by Uli Furbach as IJCAR 2006 co-program chair. Thus, there are two positions to fill.

The following candidates were nominated, and their statements are below:

Didier Galmiche ($\sim$galmiche/)
- nominated by Rajeev Gore and Frank Pfenning
Reiner Hähnle ($\sim$reiner/)
- nominated by Peter Baumgartner and Franz Baader
Aaron Stump ($\sim$stump/)
- nominated by Ting Zhang and Cesare Tinelli
Cesare Tinelli ($\sim$tinelli/)
- nominated by Robert Nieuwenhuis and Andrei Voronkov
Toby Walsh ($\sim$tw/)
- nominated by John Slaney and Graham Steel

In addition, the CADE trustees and the business meeting at CADE-20 have decided to put the following amendment of the CADE bylaws regarding the election of the CADE president to the vote of the entire AAR membership:

In Article V (Officers), Section 2 (Election and Term of Office) replace

``The President and Vice President shall be elected by and from the Board of Trustees."


``The President and Vice President shall be elected by and from the Board of Trustees using the Single Transferrable Vote system."

Statement by Didier Galmiche

I have been working in automated deduction a long time in connection with type theories, substructural logics (intuitionistic logic, and linear logic) and with interests for both proof theory and semantics. My recent works focus on methods and tools for proof and countermodel construction in various resource and separation logics and their applications to distributed systems and semi-structured data analysis.

I have some experience (PC member of logic and AR events like CSL, CADE, IJCAR, Tableaux, Wollic, co-organizer of CADE Workshops on proof-search in type-theoretic languages, member of Tableaux Steering Committee) and an approach of automated reasoning in a broad perspective (theorem proving, semantic methods, proof theory, implementations).

Therefore, as CADE trustee I could help to keep its status and audience with high standards and an attracting scope. I think that we have to continue to attract new workshop proposals on related topics, to participate to FLOC and IJCAR, and also to strengthen the relationships with related communities like logic, proof-theory, verification, or security.

Statement by Reiner Hähnle

The first international scientific conference that I attended was CADE-8 in 1986. Ever since, the CADE community has been one of the major venues where my professional career took place. My most recent contribution to CADE was a tutorial ( on verification of object-oriented software, presented at CADE-20 in Tallin this summer. In between, I participated in most CADEs, contributed numerous papers, served on several CADE PCs, and was conference chair of CADE-18 in Copenhagen.

I have worked on automated reasoning in non-classical and first-order logics in the past; my current research interests lie mainly within software verification (see the KeY project Web pages: In order to keep automated deduction a dynamic and lively field of research, I believe it is very important that CADE tries to increase the participation of consumers of reasoning technology such as formal verification or Semantic Web reasoning. This means not merely a willingness to accept papers on applications, but ideally a more proactive approach, such as the organization of special tracks or co-location with suitable events. As CADE trustee I would use my influence to make applications of automated reasoning an integral part of the conference.

In the past five years I have been deeply involved in organizing FLoC (
com/floc06/) (``hat king" of FloC 2002 - see, trustee of FLoC Inc.) and starting up IJCAR (founding member of steering committee). I also served on the steering committees of Tableaux and FTP. From this experience I gained considerable insight into the structure and current status of many subcommunities of computational logic. I believe that the field needs both: highly visible, comprehensive meetings (such as IJCAR, FLoC) as well as more intimate and specialized ones, which subcommunities can identify with. As a trustee I would work towards keeping both IJCAR and CADE as alternating events.

Statement by Aaron Stump

As a younger researcher (I got my Ph.D. in computer science from Stanford in 2002), I am very excited about the possibility of serving the automated reasoning community as a CADE trustee. I have broad interests in automated reasoning, but I am probably best known for my work in decision procedures (I was the main implementor of the CVC cooperating validity checker). I also have ongoing projects in logical frameworks, type theory, and term rewriting theory. I am particularly interested in applications of automated reasoning to verification and programming languages theory.

To me, one of the best things about CADE is the diversity of its submissions. We regularly get talks covering the range from highly theoretical to engineering focused, as well as an exciting range of applications. I find such diversity intellectually very stimulating, and as a CADE trustee, I would work to support it, for example by personally encouraging colleagues in verification and programming languages to submit to CADE. I am also supportive of the current philosophy of having CADE meet either alone, with other meetings as IJCAR, or as part of FLoC, in different years.

Statement by Cesare Tinelli

My general research interests are automated reasoning, with a focus on reasoning modulo built-in theories--that is, theories implemented by means of specialized reasoners. I have been particularly active in the combination of decision procedures and their integration into general purpose calculi. My most recent research is on the DPLL(T) scheme, a general formal framework and architecture for ground satisfiability modulo theories (SMT), and on the Model Evolution calculus, a first-order version of the DPLL procedure, of both of which I am a co-author. I'm the co-founder of the PDPAR workshop (Pragmatics of Decision Procedures in Automated Reasoning), now at its 4th edition. I have served as a PC member or co-organizer for a number of AR related events (see my Web page for a complete list), and I am currently a steering committee member of FTP, FroCoS and IJCAR.

I'm also a coordinator of the SMT-LIB initiative, whose main goal is to establish a common standard and a library of benchmarks for satisfiability modulo theories. In that capacity, I maintain active contacts with a large number of computer-aided verification practitioners and researchers from industry and academia, who have many potential applications and a strong interest for provers for satisfiability/deduction modulo theories.

As a trustee I would push for CADE to continue its efforts in attracting papers over the whole spectrum of AR research, with a renewed emphasis of attracting more work on applications. One way to achieve this at the trustees level could be to establish a set of (non-strictly binding and renewable) guidelines for future CADE PC chairs on the composition of the PC, the selection of invited speakers, and the type of solicited submissions. On a personal level, I would use my ties to the growing community of SMT researchers--which sadly seem to gravitate more and more around forums such as CAV, CP and SAT--to help maintain a continued flow of CADE submissions from them. I would also work toward making the CADE community more aware of the sort of deduction problems faced in verification today, and the need in that field of a large spectrum of deduction tools, well beyond traditional stand-alone refutational theorem provers.

As a current member of the FTP and FroCoS SC's I strongly support the idea of having a larger comprehensive event like IJCAR on a regular basis, to avoid an excessive fragmentation of the AR community into several smaller events. Consistently with that, I also support the continuted participation of CADE to FLoC as IJCAR, not as a stand-alone conference. As a CADE trustee I would also push for a better interaction and coordination between CADE and other AR events such as TABLEAUX, FTP, FroCoS. In this respect, I am in favor of maintaining a permanent IJCAR SC, made of representatives from the various events, with the main goals of coordinating the organization of IJCAR and the interaction with FLoC.

Statement by Toby Walsh

The automated reasoning (AR) community faces a number of fundamental problems. First, there is increasing fragmentation. Events like IJCAR (which I chaired in Cork in 2004) are one solution to this problem. However, we cannot stop there but must embrace other closely related areas (for example, we need to join with the satisfiability research community, in which I am very active) that have common research problems. I was very happy therefore to help get SAT 06 into the FLOC conference next year. Second, there must be more fresh blood brought into the field. I introduced a doctoral programme for IJCAR 04 to engage Ph.D. students at an early stage in their studies. However, there are other initiatives to consider, like an AR summer school. Finally, we need to maintain our visibility in related areas like KR and AI where we have much to bring to the table.

Brief bio: Toby Walsh is leader of the Knolwedge Representation and Reasoning program at National ICT Australia and a professor at UNSW. He was previously SFI Research Professor at University College Cork and an EPSRC advanced research fellow at the University of York. He completed his Ph.D. in automated reasoning at the University of Edinburgh under the supervision of Profs. Alan Bundy and Fausto Giunchiglia.

Call for Papers

AIESP 2006

The First International ICSC Symposium on Artificial Intelligence in Energy Systems and Power will be held on the island of Madeira, Portugal, February 7-10, 2006. For further information, see the website:

The organizing committee has extended the deadline for submission of papers to November 15, 2005. The conference will also accept a limited number of non-AI related poster papers.

Artificial intelligence is an advanced computer science that seeks to emulate some of the capabilities of the human brain, for example, to automate control of engineering systems and extend the skill of human operators. AIESP2006 is the first of a series of conferences on applications of AI in energy systems and power. It will provide a forum for discussing the latest developments in these subjects.

In energy systems the conference will cover topics such as alternative energy including renewable energy sources (biomass, hydro, solar, wind, geothermal, tidal and photovoltaic conversion systems), new transportation fuels (such as ethanol), and new applications of conventional energy sources (such as the use of propane and natural gas as automotive fuels, and batteries in electric vehicles), fuel cells, and gas hydrates

Examples of energy systems and power topics include dispersed generation and distribution planning, dynamic stability, load flow analysis, and power system equipment diagnosis.

Conference proceedings (including all accepted papers) will be published by ICSC Academic Press and be available for the delegates at the symposium on CD-ROM. Authors of a selected number of innovative papers will be invited to submit extended manuscripts for publication in prestigious international journals such as the International Journal of Energy Technology and Policy. For further information, please contact Ahmed Zobaa at>

Natural Language and Knowledge Representation

FLAIRS 2006 will take place at Melbourne Beach, Florida May 11-13, 2006. A special track at FLAIRS 2006 will be devoted to natural language and representation (NL-KR). Submissions are invited for this track in the following and related areas:

Only electronic submissions will be considered. Details about submission can be found on$\sim$lady0641/Flairs06_NL_KR/submission_details.html Selected papers will be considered for publication in a special journal issue of Journal of Logic and Computation in the second half of 2006. Proceedings on CD will be provided to all.

Those interested in running a demo please contact Jana Sukkarieh or Simon Dobnik

JAR Special Issue: Empirically Successful Automated Reasoning

With improving technology, theorem proving and related methods are successfully being applied to larger problems and used in more domains. To further disseminate developments and results in this area, a special issue of the Journal of Automated Reasoning dedicated to empirically successful automated reasoning will be published.

We invite submission of articles describing work on the implementation and deployment of working automated reasoning systems and applications. Both participants of the successful ESCAR-workshop at CADE-20 (see$\sim$geoff/Conferences/ESCAR/) and other authors are invited to submit contributions. Submissions should be mature journal articles. They may address any aspect of ``really working" systems and applications and should not focus on theoretical ideas that have not yet been translated into working software.

Similar to the ESCAR-workshop, this special issue will have two tracks: one for systems and one for applications. Suggested topics include the following:



Submissions should be formatted according to JAR's author guidelines (see the link on the home page below), and preferably be written in LaTeX. A LaTeX style file can be obtained from the Web: Submissions are due December 5, 2005, at The website for this special issue, containing more useful information, is

Deepak Kapur, Editor-in-Chief, Journal of Automated Reasoning
Bernd Fischer, Stephan Schulz, Geoff Sutcliffe, Guest Editors


FM'06 will be held August 21-27, 2006, in Ontario, Canada. This is the fourteenth in a series of symposia on formal methods for software development. The symposia have been notably successful in bringing together innovators and practitioners in precise mathematical methods for software development. Submissions are welcomed in the form of original papers on research and industrial experience, proposals for workshops and tutorials, entries for the exhibition of software tools and projects, and reports on ongoing doctoral work. We are particularly interested in the experience of applying formal methods in practice. The broad topics of interest of this conference are as follows:

Full papers should be submitted via the website at Accepted papers (max. 16 pages) will be published in the symposium proceedings, to appear in Springer's Lecture Notes in Computer Science series. A prize for the best technical paper will be awarded at the symposium.

Industrial Usage Reports. One day will be dedicated to sharing the experience--both positive and negative--with using formal methods in industrial environments. This year's Industry Day investigates the use of formal methods in security and trust. Invited papers on organizational and technical issues will be presented. Inquiries should be directed to the Industry Day Chairs; see the Web site for details.

Workshops. We welcome proposals for one-day or one-and-a-half-day workshops related to FM'06. In particular, but not exclusively, we encourage proposals for workshops on various application domains.

Tutorials. We are soliciting proposals for full-day or half-day tutorials. The tutorial contents can be selected from a wide range of topics that reflect the conference themes and provide clear utility to practitioners. Each proposal will be evaluated on importance, relevance, timeliness, audience appeal and past experience and qualification of the instructors.

Poster and Tool Exhibition. An exhibition of both research projects and commercial tools will accompany the technical symposium, with the opportunity of holding scheduled presentations of commercial tools.

Doctoral Symposium. For the first time, FM'06 will feature a doctoral symposium. Students are invited to submit work in progress and to defend it in front of ``friendly examiners.'' Participation for students who are accepted will be subsidized.

Submission Info

Technical Papers, Workshops, Tutorials: Friday, February 24, 2006
Posters and Tools, Doctoral Symposium: Friday, May 26, 2006


The workshop ``Methods for Modalities" (M4M) will be held in Berlin December 1-2, 2005. M4M aims to bring together researchers interested in developing algorithms, verification methods and tools based on modal logics. Here the term ``modal logics" is conceived broadly, including description logic, guarded fragments, conditional logic, and temporal and hybrid logic.

To stimulate interaction and transfer of expertise, M4M will feature a number of invited talks by leading scientists, research presentations aimed at highlighting new developments, and submissions of system demonstrations. We strongly encourage young researchers and students to submit papers and posters, especially for experimental and prototypical software tools related to modal logics.

Regular papers should not exceed 12 pages; short papers, 6 pages; and posters and tools, 2 pages. Proceedings will appear online and as a Humboldt University report. Depending on the submissions, papers may be selected to appear in a special issue of an appropriate journal. Submission is by email; either Postscript or PDF files can be sent to

For more information and registration information, see the M4M homepage at

Abstracts of Recent Theses

We are pleased to present the abstracts of three recent theses in automated reasoning.

Author: Claudio Castellini

Title: Automated Reasoning in Quantified Modal and Temporal Logics

Supervisor: Alan Smaill

Date of Defense: June 6, 2005

Institution: University of Edinburgh (UK), School of Informatics

Abstract: Quantified modal and temporal logics are extensions of classical first-order logic in which the notion of truth is extended to take into account persistence through time. Due to their high complexity, these logics are less widely known and studied than their propositional counterparts. Moreover, little so far is known about their mechanisability and usefulness for formal methods.

The relevant contributions of this thesis are threefold: firstly, we devise a sound and complete set of sequent calculi for quantified modal logics; secondly, we extend the approach to the quantified temporal logic of linear, discrete time and develop a framework for doing automated reasoning via Proof Planning in it; thirdly, we show a set of experimental results obtained by applying the framework to the problem of Feature Interactions in telecommunication systems.

These results indicate that (a) the problem can be concisely and effectively modeled in the aforementioned logic, (b) proof planning actually captures common structures in the related proofs, and (c) the approach is viable also from the point of view of efficiency.

Author: Chad E. Brown

Title: Set Comprehension in Church's Type Theory

Supervisor: Peter B. Andrews

Date of Defense: June 29, 2005

Institution: Carnegie Mellon University


hurch's simple type theory allows quantification over sets and functions. This expressive power allows a natural formalization of many mathematical concepts. However, the process of automated theorem proving in Church's type theory is more difficult than in the first-order case. One problem in particular is the instantiation of set variables. Such instantiations can involve arbitrary logical constants. Searching for set instantiations has not yet been well understood. Here we study the role of set comprehension in higher-order automated theorem proving. In particular, we introduce formulations of fragments of Church's type theory which are restricted with respect to set comprehension. We then define corresponding semantics and show soundness and completeness. Using completeness, we show that some restrictions to set comprehension are complete with respect to the usual notion of Henkin models. That is, we can prove any theorem with restricted set comprehension that could be proven with unrestricted set comprehension. We also show some restrictions are incomplete. This methodology is used to study set comprehension both in the presence and absence of extensionality.

We also describe methods for automated theorem proving in extensional type theory with restricted set instantiations. The approach to automated proof search presented here extends mating search by including connections up to extensional and equational reasoning. Search procedures based on these ideas have been implemented as part of the TPS theorem prover. The procedures have also been augmented by including the ability to solve for certain sets using set constraints. We describe the implementation and include experimental results.

The thesis can be obtained from

Author: Daniel Winterstein

Title: Using Diagrammatic Reasoning for Theorem Proving in a Continuous Domain

Supervisors: Alan Bundy, Corin Gurr, and Mateja Jamnik

Date of Graduation: January 2005

Institution: University of Edinburgh

Abstract: This project looks at using diagrammatic reasoning to prove mathematical theorems. The work is motivated by a need for theorem provers whose reasoning is readily intelligible to human beings. It should also have practical applications in mathematics teaching.

We focus on the continuous domain of analysis - a geometric subject, but one which is taught using a dry algebraic formalism which many students find hard. The geometric nature of the domain makes it suitable for a diagram-based approach. However it is a difficult domain, and there are several problems, including handling alternating quantifiers, sequences and generalisation. We developed representations and reasoning methods to solve these. Our diagram logic isn't complete, but does cover a reasonable range of theorems. It utilizes computers to extend diagrammatic reasoning in new directions, including using animation.

This work is tested for soundness, and evaluated empirically for ease of use. We demonstrate that computerised diagrammatic theorem proving is not only possible in the domain of real analysis, but that students perform better using it than with an equivalent algebraic computer system.

ANU Logic Summer School: Dec. 5-16, 2005

The Australian National University (ANU) has an exciting opportunity for IT professionals, senior educators, and students to enhance their logic and reasoning skills for the workforce, for teaching, or for higher degree by research study, in a two-week intensive summer school.

The Logic Summer School comprises a blend of practical and theoretical short courses on aspects of pure and applied logic taught by international and national experts. The school provides a unique learning experience for all participants, backed up with state-of-the-art computational science facilities at the ANU.

Program Topics:

The Summer School is intended for


Professionals: $1,650 per person; discounts are available for multiple registrations from individual companies and institutions.

Students in full-time education: $120 per person; scholarships are available and are assessed on a case-by-case basis.

Registrations after October 28, 2005, are subject to a 20% surcharge. To register or for more information visit our website at

If you would like to discuss this invitation in more detail, including advice on suitable candidacy, please contact Professor John Slaney by email: John

New Book - Rippling: Meta-Level Guidance for Mathematical Reasoning

Alan Bundy, David Basin, Dieter Hutter, and Andrew Ireland have published a new book entitled Rippling: Meta-Level Guidance for Mathematical Reasoning. Rippling was developed for inductive proofs, and it has proved applicable in problems involving reasoning about repetition (e.g., the behavior of electronic circuits over time). This book introduces researchers and graduate students to rippling and to the wider subject of automated inductive theorem proof.

Cambridge University Press, 2005, ISBN 0-521-83449-X, 202 pages

An Introduction to Rippling
Varieties of Rippling
Productive Use of Failure
A Formal Account of Rippling
The Scope and Limitations of Rippling
From Rippling to a General Methodology
Appendix 1 - An Annotated Calculus and a Unification Algorithm
Appendix 1 - Definitions of Functions Used in This Book

Gail Pieper 2005-12-01