# ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER No. 95, February 2012

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

In abstract algebra, many areas (varieties) are studied. Among such is the area known as orthomodular lattices (OMLs). The following 3-basis, in terms of the Sheffer stroke (nand), denoted by the function `f`, provides a fine target when seeking to prove some equation is a single axiom.

```f(f(x,x),f(x,y)) = x.  % absorption
f(x,f(f(y,z),f(y,z))) = f(z,f(f(y,x),f(y,x))).  % associativity
f(x,f(x,f(x,y))) = f(x,y).  % OML property
```

In 2002, Bill McCune studied orthomodular lattices with his student Michael Rose. Most impressive, they found the following single axiom.

```  f(f(f(f(y,x),f(x,z)),u),f(x,f(f(z,f(f(x,x),z)),z))) = x.  % OML-singax
```

You are challenged to prove from their axiom the given 3-basis. Then, and no doubt most intriguing, consider the following (the numbering is taken from Chapter 7 of the the book Automated Reasoning and the Discovery of Missing and Elegant Proofs, Rinton Press, 2003).

OQ04.OML
Does there exist a shorter single axiom for OML in terms of the Sheffer stroke?
CH04.OML
Is the given 23-letter single axiom for OML the only such of that length?

## Herbrand Award: Call for Nominations

Martin Giese
Secretary of AAR and CADE
On behalf of the CADE Inc. Board of Trustees

The Herbrand Award is given by CADE Inc. to honour a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to

• Larry Wos (1992)
• Woody Bledsoe (1994)
• Alan Robinson (1996)
• Wu Wen-Tsun (1997)
• Gerard Huet (1998)
• Robert S. Boyer and J Strother Moore (1999)
• William W. McCune (2000)
• Donald W. Loveland (2001)
• Mark E. Stickel (2002)
• Peter B. Andrews (2003)
• Harald Ganzinger (2004)
• Martin Davis (2005)
• Wolfgang Bibel (2006)
• Alan Bundy (2007)
• Edmund Clarke (2008)
• Deepak Kapur (2009)
• David Plaisted (2010)
• Nachum Dershowitz (2011)

A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at IJCAR 2012 is:

1st April, 2012

Nominations pending from previous years must be resubmitted in order to be considered.

Nominations should consist of a letter (preferably email) of up to 2000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent to

Franz Baader, President of CADE Inc.
baader (at) tcs.inf.tu-dresden.de

with copies to

martingi (at) ifi.uio.no

## Conferences

### IJCAR 2012 Satellite Events

IJCAR 2012, the International Joint Conference on Automated Reasoning will include the following satellite events. See here for continuously updated information.

#### Workshops

##### June 30th+July 1st:
• Workshop on Automated Theory Exploration
Jacques Fleuriot, Peter Höfner, Annabelle McIver, Alan Smaill
• Workshop on Synthesis, Verification and Analysis of Rich Models (SVARM 2012)
joint with
The 7th International Verification Workshop (VERIFY 2012)

Viktor Kuncak and Carsten Sinz
• Satisfiability Modulo Theories (SMT 2012)
Pascal Fontaine, Amit Goel

### LPAR-18, short papers and participation

The 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning will be held in Merida, Venezuela on March 11–15, 2012.

LPAR still accepts short papers of up to 5 pages in the EasyChair format, reporting on interesting work in progress or providing system descriptions. These have to be uploaded here under the Short Paper Track until February 10, 2012.

Registration is now possible on the conference web site. Early registration closes February 16.

### KI 2012, the German Conference on Artificial Intelligence

KI 2012, the 35th edition of the German Conference on Artificial Intelligence, will take place in Saarbrücken, Germany, September 24–27, 2012.

Traditionally brings together academic and industrial researchers from all areas of AI, and Reasoning is amongst the topics of interest.

Full papers are to be submitted until May 1, 2012. Accepted papers will be published in Springer's LNAI series. There is also a call for Workshop and Tutorial proposals that closes on March 15.

For further information, please refer to the conference web site.

### SAT 2012, Theory and Applications of Satisfiability Testing

The 15th Intl. Conf. on Theory and Applications of Satisfiability Testing will take place in Trento, Italy, on June 17–20th, 2012.

SAT is the primary annual meeting for researchers studying the propositional satisfiability problem, including the domains of MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean Formulae (QBF), Satisfiability Modulo Theories (SMT), Constraints Programming (CSP) techniques for word-level problems and their propositional encoding.

Regular papers (14 pages), tool presentations (6 pages), and extended abstracts/posters (2 pages) are solicited until February 12.

See the conference web page for further details.

### CSL'12, Computer Science Logic

The 21th EACSL Annual Conference on Computer Science Logic will take place in Fontainebleau, France, on September 3–6, 2012.

CSL is the annual conference of the European Association for Computer Science Logic. The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. Automated and interactive theorem proving are amongst the topics of interest.

Abstracts are to be submitted until April 2, and the full papers until April 9.

For further details, see the conference web site.

## Second International SAT/SMT Summer School

There will be a summer school on SAT, SMT, and their applications in Trento, Italy, on June 12–15th, 2012. The summer school, which boasts an impressive array of speakers, is colocated with the SAT 2012 conference.

Details about registration, etc. will soon be published om the event web site, interested students may contact the organisers, Alberto Griggio and Stefano Tonetta (griggio/tonettas (at) fbk.eu)

## Automatic Proofs for Polynomials and Special Functions

Grant Passmore and Larry C. Paulson
University of Cambridge

### Overview

A joint Cambridge-Edinburgh project is developing automatic proof procedures for mathematical assertions involving nonlinear polynomial and special function inequalities over the real numbers. Our software tools include MetiTarski, an automatic theorem prover for real-valued special function inequalities, and RAHD, a proof tool providing a rich family of customisable and heuristically combinable decision methods for real-valued nonlinear polynomial systems.

### Nonlinear Polynomial and Special Function Arithmetic

Tarski's theorem that the theory of real closed fields (RCF) admits effective elimination of quantifiers is one of the historic landmarks of mathematical logic. From this result, the decidability of elementary algebra and geometry readily follow, and a most tantalising situation arises: In principle, every elementary arithmetical conjecture over finite-dimensional Euclidean spaces may be decided simply by formalising the conjecture and asking a computer of its truth. So why then do we still not know how many unit hyperspheres may kiss in five dimensions? Is it 41? Or 42?

The issue is one of complexity. Though decidable, RCF is fundamentally infeasible. This is unfortunate, as automatic proof methods for nonlinear real arithmetic are crucially needed in both formalised mathematics and the verification of real-world cyber-physical systems. Moreover, for many such applications, RCF is insufficient: methods are needed for verifying assertions involving not only polynomials, but special functions such as log, exp and sin. This brings forth a fundamental difficulty, as, for instance, RCF extended with sin is undecidable, given that the periodicity of sin can be used to define an IsAnInteger predicate over the reals.

Despite these inherent fundamental difficulties, automatic proof methods for RCF and RCF extended with special functions can be developed which are surprisingly effective on many classes of practical problems. The development of such methods is the focus of our project. We are concurrently developing two tools: MetiTarski, for RCF extended with special functions, and RAHD, for nonlinear polynomial arithmetic.

### MetiTarski

MetiTarski is an automatic theorem prover based on a combination of resolution and a decision procedure for the theory of real closed fields. It is designed to prove theorems involving real-valued special functions such as log, exp, sin, cos and sqrt. In particular, it is designed to prove universally quantified inequalities involving such functions. Because this problem is undecidable, MetiTarski is necessarily incomplete. Nevertheless, MetiTarski is remarkably powerful. Here are a few of the hundreds of theorems that it can prove, automatically and in seconds.

MetiTarski accepts input in an extended TPTP syntax and outputs proofs in an extended TSTP syntax. Over 800 special function problems provable by MetiTarski and drawn from a variety of mathematical and engineering sources can be found in the MetiTarski distribution.

### RAHD (Real Algebra in High Dimensions)

As mentioned above, though decidable, RCF is fundamentally infeasible: By Davenport-Heinz, there exist families of n-variable RCF formulas of length O(n) whose only quantifier-free equivalences must contain polynomials of degree 2^(2^(Omega(n))) and of length 2^(2^(Omega(n))). Thus, RCF quantifier-elimination is inherently doubly exponential in dimension (the number of variables).

Given how desperately scalable RCF reasoning is needed for many verification efforts, researchers have in recent years proposed fast, sound but incomplete RCF proof procedures which are useful in various practical applications. These incomplete proof methods often have sweet spots, i.e., classes of problems for which they perform much better than they do in general (and much better than the general complete methods). Moreover, such proof procedures can often be heuristically combined and tailored to structural properties of particular classes of problems. Such combined methods are often able to solve problems which are far beyond the reach of individual methods when used in isolation.

RAHD is an RCF proof tool which uses these observations as the basis of a strategic approach to making RCF decisions. RAHD provides as primitives a vast array of (both complete and incomplete) RCF proof methods, and provides principled methods for users to build their own customised, heuristic RCF proof procedures tailored to structural properties of problem classes of interest. These combined proof methods are written using a proof strategy language, with many features similar to the approach of tactics and tacticals found in LCF-style proof assistants.

Once a RAHD proof strategy has been defined, it can then be used as a push-button automatic proof method. More information on RAHD and its many RCF proof methods can be found in Grant Passmore's 2011 University of Edinburgh Ph.D. thesis, Combined Decision Procedures for Nonlinear Arithmetics, Real and Complex.

### Request for Problems and Applications

We would appreciate hearing from researchers who believe they might benefit from the theorem proving capabilities of our tools. Given the fundamental difficulties inherent in this theorem proving domain, our work is driven by applications, and we would be delighted to work to extend our tools to handle classes of problems researchers encounter in practice.

### Obtaining our Tools

Please see our project homepage for more, including links to MetiTarski and RAHD.

### Team

The project consists of PIs Prof. Lawrence C. Paulson and Dr. Paul B. Jackson, Postdocs Dr. James Bridge and Dr. Grant Olney Passmore, and Ph.D. students William Denman, Zongyan Huang and Andrew Sogokon. The research was supported by the Engineering and Physical Sciences Research Council [grant numbers EP/I011005/1 and EP/I010335/1].