ASSOCIATION FOR AUTOMATED REASONING

• From the AAR President, Larry Wos…
• Conferences
  • CADE-24, Conference on Automated Deduction
  • CADE-24: Call for Workshops, Tutorials, and System Competitions
  • RDP 2013, Rewriting, Deduction, and Programming
  • NFM 2013, NASA Formal Methods Symposium
• Results of CADE Trustee Elections

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:

• propositional, first-order, equational, classical, higher-order, non-classical, constructive, modal, temporal, many-valued, description, meta-logics, logical frameworks, type theory, set theory, as well as any combination thereof.

Paradigms of interest include:

• theorem proving, model building, constraint solving, computer algebra, model checking, proof checking, and their integrations.

Methods of interest include:

• resolution, superposition or paramodulation, completion, saturation, term rewriting, decision procedures and their combinations, model elimination, connection method, inverse method, tableaux, induction, proof planning, sequent calculi, natural deduction, as well as their supporting algorithms and data structures, including unification, matching, orderings, indexing, proof presentation and explanation, and search plans or strategies for inference control, including semantic guidance and AI-related methods.

Applications of interest include:

• analysis, verification and synthesis of software and hardware, formal methods, computer mathematics, computational logic, declarative programming, knowledge representation, deductive databases, natural language processing, computational linguistics, ontology reasoning, robotics, planning, and other areas of artificial intelligence.

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,

• RTA, Rewriting Techniques and Applications, June 24-26, and
• TLCA, Typed Lambda Calculi and Applications, June 26-28,

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

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:

No candidate reaches at least 65 first preference votes.

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

No candidate reaches at least 65 first preference votes.

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

No candidate reaches at least 65 first preference votes.

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

No candidate reaches at least 65 first preference votes.

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

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:

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:

No candidate reaches at least 65 first preference votes.

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

No candidate reaches at least 65 first preference votes.

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

No candidate reaches at least 65 first preference votes.

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

No candidate reaches at least 65 first preference votes.

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

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:

No candidate reaches at least 65 first preference votes.

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

No candidate reaches at least 65 first preference votes.

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

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

• Franz Baader (elected 2010, president)
• Maria Paola Bonacina (CADE-24 program chair)
• Amy Felty (reelected 2010)
• Martin Giese (secretary)
• Bernhard Gramlich (elected 2012)
• Neil Murray (treasurer)
• Larry Paulson (elected 2010)
• Brigitte Pientka (elected 2010)
• Renate Schmidt (reelected 2012, vice-president)
• Viorica Sofronie-Stokkermans (elected 2011)
• Geoff Sutcliffe (elected 2011)
• Christoph Weidenbach (relected 2012)

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!