ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER No. 99, October 2012

From the AAR President, Larry Wos…

Algebra is in focus again; geometry will follow soon.

From the viewpoint of automated reasoning and, in a different way, from the viewpoint of mathematics, when asked to find a proof for a theorem, you have three choices. You can proceed as is often done in a class by starting with the axioms, make one deduction after another, and conclude with the desired result. In other words, you can produce a forward proof. Instead, you could deny the conclusion of the theorem, work backward, and, if successful, produce a deduction that contradicts some axiom. In this case, you have a backward proof. Or, as you have surmised, you can seek a bidirectional proof, working forward from the axioms and backward from the denial of the conclusion.

One of the piquant, or annoying, properties of automated reasoning is encountered when you have a bidirectional proof and wish, instead, to have a forward proof. Especially (but not exclusively) when paramodulation is the inference rule, you can be offered theorems to prove for which you can find a bidirectional proof, perhaps with some effort, but for which finding a forward proof will be most challenging. One reason is that if you simply give a program permission to paramodulate from or into a variable, with no constraints, the program can drown. Yes, paramodulation is indeed sinister.

In this column, I offer you such a theorem. The theorem focuses on ring theory. You are first challenged to find a proof, any proof. Then, more challenging, you are asked to find a forward proof.

x = x.

%  Ring axioms
0 + x = x.
x + 0 = x.
m(x) + x = 0.
x + m(x) = 0.
(x + y) + z = x + (y + z).
x + y = y + x.
(x * y) * z = x * (y * z).
x * (y + z) = (x * y) + (x * z).
(y + z) * x = (y * x) + (z * x).

%  a multiplicative unit
x * 1 = x.
1 * x = x.

%  Theorem:  If 1-ab has an inverse, then 1-ba has an inverse.
%  formally, (all a all b (
%        (exists c ((1 + m(a * b)) * c = 1))
%           ->
%        (exists x ((1 + m(b * a)) * x = 1))))
%
%  denial of theorem in an OTTER notation:
(1 + m(a * b)) * c = 1.
(1 + m(b * a)) * x != 1 | $ANSWER(x).
%  (The answer literal tells us the inverse of 1-ba in terms of a, b, and c.)

If and when success is yours, a nice research topic focuses on finding a procedure—not necessarily an algorithm—for converting bidirectional proofs to forward.

Conferences

CADE-24, Conference on Automated Deduction

The 24th International Conference on Automated Deduction will be held in Lake Placid, New York, USA on 9–14 June 2013.

CADE is the major forum for the presentation of research in all aspects of automated deduction. The conference invites high-quality submissions on the general topic of automated reasoning, including foundations, applications, implementations and practical experiences.

Logics of interest include:

Paradigms of interest include:

Methods of interest include:

Applications of interest include:

The CADE program will include the annual CADE ATP System Competition (CASC), as well as various workshops and tutorials. Details will be published in separate calls and on the conference website.

CADE calls for regular papers of up to 15 pages and system descriptions of up to 7 pages. Full system descriptions that provide in-depth presentation of original ideas in an implemented system can be submitted as regular papers.

Papers shall be submitted until 14 January 2013. An abstract must be submitted already on 7 January 2013. Accepted papers will be published in Springer's LNCS series.

Please refer to the conference web site for further information, including the full Call for Papers.

CADE-24: Call for Workshops, Tutorials, and System Competitions

CADE-24 is soliciting proposals for workshops, tutorials, and system competitions to be held in conjunction with CADE-24.

Proposals should be submitted until 9 November 2012, and notifications are scheduled to be sent out on 30 November 2012.

The conference web site contains details about required information, submission procedure, etc.

RDP 2013, Rewriting, Deduction, and Programming

RDP 2013, the seventh Federated Conference on Rewriting, Deduction, and Programming, will take place on 23–28 June 2013 in Eindhoven, The Netherlands. RDP 2013 will consist of two main conferences,

and several workshops.

RTA 2013, the 24th International Conference on Rewriting Techniques and Applications, is the major forum for the presentation of research on all aspects of rewriting, including applications, foundations, frameworks, and implementations. Papers of at most 10 pages for system descriptions, and 15 pages for regular papers in LIPIcs style, are to be submitted by 5 February 2013, with abstracts due on 1 February.

TLCA 2013, the 11th International Conference on Typed Lambda Calculi and Applications is a forum for original research in the theory and applications of typed lambda calculus, broadly construed, including the whole range of applicable proof theory, semantics, type systems, and connections to programming. Research papers of up to 15 pages shall be submitted by 1 February 2013, with abstracts registered until 25 January 2013.

Further information is available via the RDP web site.

NFM 2013, NASA Formal Methods Symposium

The 5th NASA Formal Methods Symposium (NFM) will take place at the NASA Ames Research Center at Moffett Field, CA, USA on 14–16 May 2013.

The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other safety-critical systems.

The symposium encourages submissions on cross-cutting approaches that bring together formal methods and techniques from other domains such as probabilistic reasoning, machine learning, control theory, robotics, and quantum computing among others. Formal verification, including theorem proving is amongst the areas of interest.

The paper submission deadline is 7 December 2012.

Please refer to the symposium web page for full details.

Results of CADE Trustee Elections

Martin Giese
(Secretary of AAR and CADE)
E-mail: martingi (at) ifi.uio.no

An election was held from 6 August through 9 September 2012 to fill three positions on the board of trustees of Cade, Inc. Rajeev Goré, Bernhard Gramlich, Konstantin Korovin, Christopher Lynch, Renate Schmidt, and Christoph Weidenbach were nominated.

Ballots were sent by electronic mail to all members of AAR on 6 August, for a total of 993 ballots. Of these, 129 were returned with a vote, representing a participation level of 13.0% (as compared to 16.2% in 2011, 13.3% in 2010, 18.3% in 2009, 18% in 2008, 16.4% in 2007, and 16.0% in 2006). All votes were valid.

Therefore, in each iteration of the single transferrable vote algorithm described in the CADE Bylaws, a candidate is elected iff she or he gets at least 65 1st preference votes. Otherwise, the votes of the candidate with the least 1st preference votes are redistributed.

The following table reports the initial distribution of preferences among the candidates:

Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. no supp.
Rajeev Goré 22 17 28 15 17 18 12
Bernhard Gramlich 26 19 19 21 14 9 21
Konstantin Korovin 17 17 16 20 14 16 29
Christopher Lynch 15 17 22 18 13 19 25
Renate Schmidt 22 36 17 12 17 8 17
Christoph Weidenbach 27 21 19 17 14 9 22

No candidate reaches at least 65 first preference votes.

By redistributing the votes of Christopher Lynch, one gets the following table:

Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. no supp.
Rajeev Goré 23 24 28 18 24 12
Bernhard Gramlich 33 14 27 22 12 21
Konstantin Korovin 19 23 16 19 23 29
Renate Schmidt 24 41 18 20 9 17
Christoph Weidenbach 30 24 24 16 13 22

No candidate reaches at least 65 first preference votes.

By redistributing the votes of Konstantin Korovin, one gets the following table:

Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. no supp.
Rajeev Goré 27 32 25 33 12
Bernhard Gramlich 37 18 33 20 21
Renate Schmidt 28 50 18 16 17
Christoph Weidenbach 37 26 25 19 22

No candidate reaches at least 65 first preference votes.

By redistributing the votes of Rajeev Goré, one gets the following table:

Candidate 1st pref. 2nd pref. 3rd pref. no supp.
Bernhard Gramlich 43 32 33 21
Renate Schmidt 41 47 24 17
Christoph Weidenbach 43 33 31 22

No candidate reaches at least 65 first preference votes.

By redistributing the votes of Renate Schmidt, one gets the following table:

Candidate 1st pref. 2nd pref. no supp.
Bernhard Gramlich 61 47 21
Christoph Weidenbach 61 46 22

No candidate reaches at least 65 first preference votes.

The two remaining candidates have the same number of 1st preference votes. In this case, the CADE STV algorithm requires redistributing the votes of the candidate with the fewest 2nd preference votes.

By redistributing the votes of Christoph Weidenbach, one gets the following table:

Candidate 1st pref. no supp.
Bernhard Gramlich 108 21

Now, Bernhard Gramlich reaches at least 65 first preference votes, and is elected.

To find the next elected candidate, we redistribute the votes of Bernhard Gramlich and get the following table:

Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. no supp.
Rajeev Goré 26 24 25 23 19 12
Konstantin Korovin 18 26 19 19 18 29
Christopher Lynch 25 14 24 20 21 25
Renate Schmidt 29 37 18 15 13 17
Christoph Weidenbach 31 23 26 18 9 22

No candidate reaches at least 65 first preference votes.

By redistributing the votes of Konstantin Korovin, one gets the following table:

Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. no supp.
Rajeev Goré 30 30 31 26 12
Christopher Lynch 28 20 30 26 25
Renate Schmidt 34 44 15 19 17
Christoph Weidenbach 37 28 28 14 22

No candidate reaches at least 65 first preference votes.

By redistributing the votes of Christopher Lynch, one gets the following table:

Candidate 1st pref. 2nd pref. 3rd pref. no supp.
Rajeev Goré 37 36 44 12
Renate Schmidt 45 44 23 17
Christoph Weidenbach 46 35 26 22

No candidate reaches at least 65 first preference votes.

By redistributing the votes of Rajeev Goré, one gets the following table:

Candidate 1st pref. 2nd pref. no supp.
Renate Schmidt 61 51 17
Christoph Weidenbach 58 49 22

No candidate reaches at least 65 first preference votes.

By redistributing the votes of Christoph Weidenbach, one gets the following table:

Candidate 1st pref. no supp.
Renate Schmidt 112 17

Now, Renate Schmidt reaches at least 65 first preference votes, and is elected.

To find the next elected candidate, we redistribute the votes of Renate Schmidt and get the following table:

Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. no supp.
Rajeev Goré 36 30 27 24 12
Konstantin Korovin 24 35 20 21 29
Christopher Lynch 32 19 29 24 25
Christoph Weidenbach 37 36 22 12 22

No candidate reaches at least 65 first preference votes.

By redistributing the votes of Konstantin Korovin, one gets the following table:

Candidate 1st pref. 2nd pref. 3rd pref. no supp.
Rajeev Goré 44 39 34 12
Christopher Lynch 35 37 32 25
Christoph Weidenbach 50 37 20 22

No candidate reaches at least 65 first preference votes.

By redistributing the votes of Christopher Lynch, one gets the following table:

Candidate 1st pref. 2nd pref. no supp.
Rajeev Goré 56 61 12
Christoph Weidenbach 69 38 22

Now, Christoph Weidenbach reaches at least 65 first preference votes, and is elected.

To summarize, the three candidates elected are Bernhard Gramlich, Renate Schmidt, and Christoph Weidenbach.

After this election, the following people (listed alphabetically) are serving on the board of trustees of CADE Inc.:

On behalf of the AAR and CADE Inc., I thank Rajeev Goré for his services as a trustee during the last three years.

I further thank all candidates for running in the election, and all members who voted.

Congratulations to Bernhard Gramlich, Renate Schmidt, and Christoph Weidenbach on being elected!