Proof length has long been of interest to mathematicians and logicians. For example, the logician C. A. Meredith devoted considerable effort in finding so-called short proofs, and logicians who followed him (including A. Prior and my colleagues D. Ulrich and J. Halleck) took up the activity. Algebraists, including S. Stein and, on occasion, Bill McCune, were also interested in finding short proofs.
In the early 1950s, A. Weil produced a proof requiring but four and a half lines showing that the Cartesian product of compact spaces is compact. If I could produce that proof, which I cannot, I conjecture that few if any could follow it. Indeed, at the time (when I was a student at the University of Chicago in the mathematics department), the mimeographed proof that was handed out took more than eight pages, if memory serves.
But what is meant by proof length? By length, I do not include the axioms used in a proof; rather, I count merely the deduced equations or deduced formulas. But a bit of confusion still remains.
If you consider a proof obtained with a Knuth-Bendix approach, proof length can be most misleading. At least with OTTER, the demodulations that occur are not counted as proof steps. Therefore, you can have two proofs, each of length 20, say, but such that one proof takes two pages to present, while the other takes six pages to present. The two-page proof may apply a lot of demodulation, perhaps more than one application at each step. Indeed, McCune once had a few-step proof that involved 500 demodulation steps!
What I like is a proof that uses paramodulation alone, with no demodulation. In such a proof, all the steps are presented explicitly, giving a more realistic idea of proof length.
With this preamble, I now offer two challenges.
First recall that a group has exponent 5 when the fifth power of x for all elements x is the identity e. Such groups admit a single axiom. Here is a single axiom for groups of exponent 5.
(f(x,f(x,f(f(x,f(x,f(f(x,y),z))),f(e,f(z,f(z,f(z,z))))))) = y).
Now here is the negation of the join of what is to be proved with a Knuth-Bendix approach.
(f(f(a,b),c) != f(a,f(b,c))) | (f(e,a) != a) | (f(a,f(a,f(a,f(a,a)))) != e) | $ANS(all).
Deriving a Knuth-Bendix proof is the first challenge.
The second challenge is to take your proof and convert it into a proof in which no demodulation occurs. Alternatively, you might produce a proof in which Knuth-Bendix is not used, one indeed in which demodulation is absent. You might choose to rely on paramodulation exclusively.
We would like to remind our readers that Herbrand Award nominations are solicited until
1st April, 2012
Details about the award and the nomination procedure are given in the previous newsletter.
The Alan Turing Centenary Conference will be held at the University of Manchester, UK, on 22–25 June 2012. The conference aims
It will feature
Registration opens on 1st March 2012. The number of participants is limited.
Extended abstracts can be submitted until 15 March 2012.
For more details, please check the conference web page.
The 10th International Workshop on User Interfaces for Theorem Provers (UITP 2012) will be held in Bremen, Germany on 11 July 2012 as part of CICM 2012.
UITP invites contributions from the theorem proving, formal methods and tools, and HCI communities, both to report on experience with existing systems, and to discuss new directions. The submission deadline is 1st May 2012.
Please refer to the workshop web page for details.
The 28th British Colloquium for Theoretical Computer Science will be hosted held at the University of Manchester on 2–5th April 2012.
The purpose of BCTCS is to provide a forum in which researchers in theoretical computer science can meet, present research findings, and discuss developments in the field. It also aims to provide an environment in which PhD students can gain experience in presenting their work, and benefit from contact with established researchers.
Abstracts of contributed talks should be submitted until 19 March.
Full details are available from the colloquium web page
The third Workshop on Practical Aspects of Automated Reasoning will be held in Manchester, UK, on 30 June 2012 (preliminary). PAAR will be associated with IJCAR-2012, which is held as part of the Alan Turing Year 2012, just after The Alan Turing Centenary Conference.
PAAR provides a forum for developers of automated reasoning tools to discuss and compare different implementation techniques, and for users to discuss and communicate their applications and requirements.
Short abstracts of up to 10 pages can be submitted until 16 April 2012.
See the workshop web page for details.
The 2nd Joint International Workshop on Strategies in Rewriting, Proving and Programming will be held in Manchester, UK, on 1 July 2012.
The workshop aims at facilitating synergies between research on strategies in automated reasoning, programming languages and software verification. Amongst others, work on strategies in both automated and interactive reasoning systems is of interest, as well as work on the evaluation and analysis of strategies or on strategy languages.
The submission deadline is 9 April 2012. After the workshop, authors of accepted abstracts are invited to submit a full version (max 15 pages), which is refereed again for inclusion in the final workshop proceedings, which the organisers expect to publish with EPTCS.
For details, please refer to the workshop web page.
The 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems will take place in Manchester, UK, on 30 June 2012, as part of IJCAR.
The aim of the workshop is to investigate empirical approaches and criteria for effective comparative evaluation of reasoning systems. Topics of interest include e.g., comparative case studies, criteria for empirical evaluation, design, organisation, and conclusions from competitions, etc. Reports on evaluating a single system are not in scope.
Full details are available from the workshop web site.