# ASSOCIATION FOR AUTOMATED REASONING

## From the AAR President, Larry Wos...

AAR is now entering a new exciting phase of its existence. The plan is to expand the activities of AAR, to provide a focus point for the broad AR community, and to provide services and support for research. For one important item, we now have a new editor of the newsletter, Martin Giese. We in AAR are indeed fortunate to have him and his expertise. I, for one, welcome him on board. I eagerly await to witness his influence on the content of the newsletter. Please transmit to Martin Giese items that might be of use to our membership. His e-mail address is `martingi (at) ifi.uio.no`

I offer a challenge to students, professors, and others in general. For the first person, or group, that meets this challenge I shall give a prize of \$100. The field in focus is called Lukasiewicz's infinite-valued sentential calculus. The following clauses provide an axiom system.

```
%  Just the implicational Axioms: MV1 - MV3
P(i(x,i(y,x))).
P(i(i(x,y),i(i(y,z),i(x,z)))).
P(i(i(i(x,y),y),i(i(y,x),x))).
%  Following is MV4.
P(i(i(n(x),n(y)),i(y,x))).
```

One additional axiom, the following, is sometimes given.

```  %  Following is MV5.
P(i(i(i(x,y),i(y,x)),i(y,x))).
```

As it turns out, MV5 is dependent on the other four formulas. I have a number of 30-step proofs, each relying on condensed detachment. The challenge is to find a proof relying strictly on condensed detachment where the proof has length 29 or less (deduced steps). You can have a reasoning program apply condensed detachment by using the inference rule hyperresolution and the following clause, where `|` denotes logical or and `-` denotes logical not.

```  -P(i(x,y)) | -P(x) | P(y).
```

At this point in time, I have not included a 30-step proof in order to avoid biasing you. Good luck. Yes, I am indeed very interested in a proof sorter than length 30.

## AAR News

### Thanking the Previous Editor

For many years, AAR has been more than fortunate to have Gail Pieper be editor of the newsletter. She has set a standard that we can ask future editors to follow. For those years of service, we thank you. Gail, from all of the members of AAR, we are indebted to you and know that, whatever activity you decide to pursue, you will succeed.

Larry Wos
on behalf of the board of the AAR

### New Web Pages of the AAR

The AAR web pages have been ported to http://www.AARInc.org/. The pages include the names and contact information of the board members, the (soon to be updated) bylaws, the membership list, all newsletters, and information about the Herbrand Award. Visit http://www.AARInc.org/ now, if only to see the new AAR logo!

### New Members in the Board of the AAR

The board of the AAR has five members: president, vice president, secretary, and two CADE nominees. Until recently, CADE has been represented by Alan Bundy and Deepak Kapur. Both have stepped down, after many years of service. As successors, the CADE trustees elected Maria Paola Bonacina and Geoff Sutcliffe. The AAR board now has the following composition:

• Larry Wos — President
• Hans Jürgen Ohlbach — Vice-president
• Maria Paola Bonacina — CADE nominee
• Geoff Sutcliffe — CADE nominee
• Wolfgang Ahrendt — Secretary

On the behalf of AAR and CADE, I thank Alan Bundy and Deepak Kapur for everything they did in service of both associations.

Wolfgang Ahrendt

## Herbrand Award

It is my distinct honor to announce on behalf of the Board of Trustees of CADE Inc. that Edmund M. Clarke is to receive the 2008 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of his role in the invention of model checking and his sustained leadership in the area for more than two decades.

The award will be presented to Professor Clarke at the 4th International Joint Conference on Automated Reasoning (IJCAR 2008) in Sydney, Australia.

## Woody Bledsoe Student Travel Awards

The Woody Bledsoe Student Travel Award is intended to enable selected students to attend the the International Joint Conference on Automated Reasoning (IJCAR) by covering much of their expenses. The winners of the travel award will be (partially) reimbursed for their conference registration, transportation, and accomodation expenses (past awards have varied, but have typically been AU\$250 to AU\$1000). Preference will be given to students who will play an active role in the conference, including satellite workshops, and do not have alternative funding. However, also students in other situations are very much encouraged to apply.

See The IJCAR 2008 web pages for more information, including application details.

## Symposium in Honour of Alan Bundy

The University of Edinburgh School of Informatics is holding a symposium to celebrate Alan Bundy's 60th birthday on July 13th and 14th 2008.

The broad range of Alan's research interests will be reflected in the invited talks by top international researchers who have worked closely with Alan over the years: Jörg Siekmann, Fausto Giunchiglia, Frank van Harmelen, Luigia Aiello, Chris Mellish, Dave Robertson, Stan Wainer and Alan Smaill. There will be public lectures on the Future of AI and many opportunities for informal conversation as well as round table discussions. This will also be the first event showcasing the new University of Edinburgh Informatics Forum.

Attendance is free and there will be a celebratory dinner on July 13th and a ceilidh on July 14th. We have funding for PhD students from AISB and from EPSRC to cover accommodation and travel. Further information and registration is available online here.

Please register by the 24th of June!

Any questions concerning the event can be sent to Sofi Freijeiro-Mato (`sfmato (at) inf.ed.ac.uk`.

## Workshops

### Workshops at IJCAR 2008

We would like to remind you that IJCAR 2008 will host a number of exciting workshops:

Note that the ESHOL workshop has been merged into PAAR 2008, and that the workshop on Combining Systems for Efficient and Scalable Reasoning (CoSyScaRe 08) has been cancelled.

### User Interfaces for Theorem Provers

The 8th International Workshop On User Interfaces for Theorem Provers will be held as a TPHOLS'08 Satellite Workshop in Montréal, Québec, Canada, on Friday, 22nd August 2008. The UITP workshop series brings together researchers interested in designing, developing and evaluating interfaces for interactive proof systems, such as theorem provers, formal method tools, and other tools manipulating and presenting mathematical formulas. Topics covered include, but are not limited to:

• Application-specific interaction mechanisms or designs for prover interfaces
• Experiments and evaluation of prover interfaces
• Languages and tools for authoring, exchanging and presenting proof
• Implementation techniques (e.g. web services, custom middleware, DSLs)
• Integration of interfaces and tools to explore and construct proof
• Representation and manipulation of mathematical knowledge or objects
• Visualisation of mathematical objects and proof
• System descriptions

### Automated Deduction in Geometry

The Workshop on Automated Deduction in Geometry (ADG) will be held at East China Normal University, Shanghai, China, on September 22–24, 2008.

The workshop is a leading international forum to exchange ideas and views, to present research results and progress, and to demonstrate software tools on the intersection between geometry and automated deduction. The main objective of this workshop is to encourage/promote/guide research efforts in the area in an informal setting.

It is expected that the accepted full papers will be published as a special issue of some journal or in the Springer Lecture Notes in Artificial Intelligence (LNAI) series

Specific topics for ADG 2008 include (but are not limited to):

• Polynomial algebra, invariant and coordinate-free methods, probabilistic, synthetic, and logic approaches, techniques for automated geometric reasoning from discrete mathematics, combinatorics, and numerics.
• Symbolic and numeric methods for geometric computation, geometric constraint solving, automated generation/reasoning and manipulation with diagrams.
• Design and implementation of geometry software, special-purpose tools, automated theorem provers, experimental studies.
• Applications of ADG to mechanics, geometric modeling, CAGD/CAD, computer vision, robotics, and education.

Visit the workshop web pages for detailed information.

### Empirically Successful Automated Reasoning for Mathematics

The CICM 2008 Workshop on Empirically Successful Automated Reasoning for Mathematics (ESARM) will be held as part of the Conferences on Intelligent Computer Mathematics, in Birmingham, UK, 26th July–2nd August, 2008.

This workshop will bring together practioners and researchers who are concerned with the development and application of automated reasoning for mathematics. The workshop will discuss only "really running" systems and applications, and not theoretical ideas that have not yet been translated into working software.

See the workshop web pagefor details.

## Conferences

### IJCAR 2008

The The 4th International Joint Conference on Automated Reasoning, IJCAR 2008, will be held in Sydney, Australia, 10th–15th August 2008. The conference is a merger of four leading conferences and workshops:

• CADE (Conference on Automated Deduction),
• FroCoS (Symposium on Frontiers of Combining Systems),
• FTP (Workshop on First-order Theorem Proving) and
• TABLEAUX (Conference on Analytic Tableaux and Related Methods)

IJCAR is the premier international joint conference on all aspects of automated reasoning, including foundations, implementations, and applications. The IJCAR technical program will consist of presentations of high-quality original research papers and invited talks. There will be two days of workshops and tutorials, 10th and 11th August, and the conference 12th to 15th August.

See The IJCAR Web pages for detailed information, including 101 reasons to attend the conference!

### Logic for Programming, Artificial Intelligence and Reasoning (LPAR)

The 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) will be held at Doha, Qatar, on November 23–27, 2008.

New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to:

 Automated reasoning Computional interpretations of logic Constraint programming Constructive logic and type theory Decision procedures Description logics Foundations of security Implementations of logic Interactive theorem proving Knowledge representation and reasoning Lambda calculus Logic and automata Logic and computational complexity Logic and databases Logic and games Logic for the semantic web Logical aspects of concurrency Logical foundations of programming Logic in artificial intelligence Logic of distributed systems Logic programming Modal and temporal logics Model checking Non-monotonic reasoning Ontologies Program and system verification Proof assistants Proof-carrying code Proof planning Proof theory Propositional satisfiability Reasoning about actions Rewriting and unification Satisfiability modulo theories Static analysis of programs Specification using logics Translation validation

More details can be found on the LPAR web pages.

### Theorem Proving in Higher Order Logics (TPHOLs)

The 21st International Conference on Theorem Proving in Higher Order Logics will be take place in Montéal, Québec, Canada, on 18th–21st August, 2008.

The conference covers all aspects of theorem proving in higher order logics, and related topics in theorem proving and verification. This includes, but is not limited to, the following topics:

• Formal semantics of specification, modelling, and programming languages: formal synthesis, validated compilation, formal design flows.
• Specification and verification of hardware: microprocessors, memory systems, buses, pipelines etc.
• Specification and verification of software: program verification, refinement, and synthesis for functional, declarative and imperative languages; proof carrying code.
• Formalisation of mathematical theories.
• Advances in theorem prover technology: proof automation and decision procedures, induction, combination of deductive and algorithmic approaches, incorporation of theorem provers into larger systems, combination of theorem provers with other provers and tools.
• Industrial application of theorem provers.
• Proof Pearls: concise and elegant presentations of interesting examples.
• Other topics, including: security algorithms, properties, and policies; specification and requirements analysis of systems; user interfaces for theorem provers; development and extension of higher order logics.

See the TPHOLs 2008 web pages for more details.

### Integrated Formal Methods iFM 2009

The conference on integrated formal methods, iFM 2009, will take place in Düsseldorf, Germany, on 16th–19th February 2009.

The iFM conference series seeks to further research into the combination of different formal methods, both for modelling and analysis, covering all aspects from language design over verification techniques to tools and their integration into software engineering practice.

Areas of interest include but are not limited to:

• Formal and semiformal modelling notations
• Semantics
• Verification
• Model checking
• Static analysis
• Theorem proving
• Integration of formal methods into software engineering practice
• Refinement
• Model transformations
• Type systems
• Logics
• Tools
• Experience reports
• Case studies

## JAR Special Issue On Operating Systems Verification

There will be a special issue of the Journal of Automated Reasoning on Operating Systems Verification. The submission deadline is September 15, 2008.

Industrial-strength software analysis and verification has advanced in recent years through the introduction of model checking, automated and interactive theorem proving, static analysis techniques, as well as correctness by design. However, many techniques are working under restrictive assumptions which are invalidated by complex (embedded) system software such as operating system kernels, low-level device drivers or microcontroller code.

This special issue will be devoted to the formal verification of operating systems and similar low-level systems code. The emphasis is on techniques and methods that provide real solutions to real software problems. A real solution is one that is applicable to the problem in industry and not one that only applies to an abstract, academic toy version of it. Submissions are encouraged, but not limited to, the following topics and their application to operating systems or low-level systems code:

• model checking
• automated and interactive theorem proving
• embedded systems development
• programming languages
• verifying compilers
• software certification