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