NEWSLETTER No. 95, February 2012

- From the AAR President, Larry Wos...
- Herbrand Award: Call for Nominations
- Conferences
- Second International SAT/SMT Summer School
- Automatic Proofs for Polynomials and Special Functions

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?

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

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

**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

**Workshop on Comparing Logical Decision Methods (CLoDeM 2012)**

Valentin Goranko and Martin Lange**Practical Aspects of Automated Reasoning (PAAR 2012)**

Pascal Fontaine, Renate A. Schmidt and Stephan Schulz**Proof eXchange for Theorem Proving (PxTP 2012)**

David Pichardie and Tjark Weber**The 4th International Workshop on Invariant Generation (WING 2012)**

Gudmund Grov and Thomas Wies**The 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE 2012)**

Bernhard Beckert, Armin Biere, Vladimir Klebanov and Geoff Sutcliffe**Uncertainty in Description Logics (UniDL 2012)**

Anni-Yasmin Turhan, Thomas Lukasiewicz and Rafael Peñaloza

**The 2nd Joint International Workshop on Strategies in Rewriting, Proving and Programming (IWS 2012)**

Maria Paola Bonacina and Maribel Fernandez**Workshop on Logics for Resources, Processes, and Programs (LRPP 2012)**

Didier Galmiche and David Pym**The 26th International Workshop on Unification (UNIF 2012)**

Santiago Escobar, Konstantin Korovin and Vladimir Rybakov**StarExec**

Aaron Stump, Cesare Tinelli and Geoff Sutcliffe**OWL Reasoner Evaluation Workshop**

Ian Horrocks, Mikalai Yatskevich and Ernesto Jiménez-Ruiz**Automated Reasoning for Enterprise Information Systems**(**AREIS 2012**)

Peter Baumgartner and Silvio Ranise

**CADE ATP System Competition (CASC-J6)**

Geoff Sutcliffe**SMT Competition (SMT-COMP 2012)**

Roberto Bruttomesso, David R. Cok and Alberto Griggio**Termination Competition 2012**

Albert Rubio and René Thiemann**OWL Reasoner Evaluation**

Ian Horrocks, Mikalai Yatskevich and Ernesto Jiménez-Ruiz

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

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.

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.

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)

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.

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

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

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.

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

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