ASSOCIATION FOR AUTOMATED REASONING

From the AAR President, Larry Wos…

In the preceding column, you were challenged to find a proof of a theorem suggested by Ross Overbeek, the four-point theorem. You were asked to rely on one of Tarski's axiom systems. In the theorem, you are told that points `a3` and `a6` are each between `a2` and `a4`. You are asked to prove either `T(a2,a3,a6)` or `T(a2,a6,a3)`, where `T` denotes betweenness. Here is one representation of the theorem.

```T(a2,a3,a4).
T(a2,a6,a4).
-T(a2,a3,a6)|\$ANS(CH5A).
-T(a2,a6,a3)|\$ANS(CH5B).
```

Now, in response to the curiosity of some, if a proof has not been found, is there a trick to finding such a proof?

Well, when I failed repeatedly with OTTER, I turned to Michael Beeson. He suggested, as you will see, that a point should be defined that extends an appropriate line. The following clause turns out to be most useful. You might say a trick was needed, and here is a superb trick.

```q = f4(a4,a2,a4,a2).
```

If you add this clause to those that did not yet yield a proof, voila!

But, especially for those who enjoy challenges, and perhaps geometry, I offer two additional challenges in Tarskian geometry. You are asked to prove the following two theorems. Keep in mind that `T` denotes betweenness, not strictly, and `E` denotes equidistance. I offer them in the order of difficulty.

```xq = xa | -T(xq,xa,u) | -E(xa,u,xc,xd) | f4(xq,xa,xc,xd) = u.    % Satz 2.12

-T(xa,xb,xc) | -T(xa1,xb1,xc1) | -E(xa,xb,xa1,xb1) | -E(xb,xc,xb1,xc1) | E(xa,xc,xa1,xc1).  % Satz 2.11
```

Yes, more difficult theorems do indeed exist, perhaps offered in future newsletters.

Herbrand Award: Call for Nominations

Martin Giese
On behalf of the CADE Inc. Board of Trustees

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)
• Melvin Fitting (2012)

A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at CADE-24 is:

15th March 2013

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

with copies to

Martin Giese, Secretary of CADE Inc. and AAR
martingi (at) ifi.uio.no

Conferences

RTA 2013, Rewriting Techniques and Applications

The 24th International Conference on Rewriting Techniques and Applications will be held in Eindhoven, Netherlands on 24–26 June 2013.

RTA 2013 is organised as part of the Federated Conference on Rewriting, Deduction, and Programming (RDP 2013), together with the 11th International Conference on Typed Lambda Calculi and Applications (TLCA 2013), and several related events.

Full details are available on the website.

CSL'13, Computer Science Logic

The 22nd EACSL Annual Conference on Computer Science Logic will take place in Torino, Italy, on 2nd–5th September 2013.

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 1st April, and the full papers until 9th April.

For further details, see the conference web site.

FMCAD 2013, Formal Methods in Computer-Aided Design

FMCAD 2013 will be co-located with Memocode, the ACM/IEEE International Conference on Formal Methods and Models for Codesign, in Portland, Oregon, USA. Memocode will take place from October 18 to 19, followed by a joint FMCAD/Memocode tutorial day on October 20. FMCAD will continue from October 21 to 23, 2013.

FMCAD 2013 is the thirteenth in a series of conferences on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.

Workshops

The following workshops will be held in connection with the CADE-24 conference in Lake Placid, New York, 9–10 June, 2013.

For up to date details, please refer to the CADE workshop web page.

ADDCT, Automated Deduction: Decidability, Complexity, Tractability

Decidability, and especially complexity and tractability of logical theories is extremely important for a large number of applications. Although general logical formalisms (such as predicate logic or number theory) are undecidable, decidable theories or decidable fragments thereof (sometimes even with low complexity) often occur in mathematics, in program verification, in the verification of reactive, real time or hybrid systems, as well as in databases and ontologies. It is therefore important to identify such decidable fragments and design efficient decision procedures for them. It is equally important to have uniform methods (such as resolution, rewriting, tableaux, sequent calculi,…) which can be tuned to provide algorithms with optimal complexity.

The goal of ADDCT is to bring together researchers interested in

• identifying (fragments of) logical theories which are decidable, identifying fragments thereof which have low complexity, and analysing possibilities of obtaining optimal complexity results with uniform tools;
• analysing decidability in combinations of theories and possibilities of combining decision procedures;
• efficient implementations for decidable fragments;
• application domains where decidability resp. tractability are crucial.

Full Paper submission: March 26, 2013
Final versions: May 10, 2013
Workshop: June 10, 2013

ARSEC, Automated Reasoning in Security

Automated reasoning methods have become increasingly critical in many areas of security, from analysing cryptographic protocols for flaws to analysing access-control and privacy policies. This interaction is proving to be mutually beneficial: automated reasoning methods are finding new applications in security; and new automated reasoning methods, developed for security applications, are enriching the tools available to all areas of automated reasoning.

ARSEC will bring together researchers interested in automated reasoning and security to present recent work (including work in progress) and to discuss new ideas and trends in the field.

Possible topics include, but are not limited to:

• Security Protocols;
• Security Policies;
• Privacy and Confidentiality;
• Intrusion Detection;
• Automated Reasoning techniques such as Paramodulation, Rewriting, Unification and Satisfiability Modulo Theories (SMT).

Paper submission: 25 March 2013
Workshop: 9 June 2013

ARiSVe, Automated Reasoning in Software Verification

The focus of the workshop is application of automated reasoning in the context of software verification, and, more generally, automation in software verification. Relevant topics include but are not limited to:

• specifics of verification-related automated reasoning tasks;
• efficient translation of high-level verification conditions to logical languages of automated reasoning tools;
• handling of the prover's feedback: proofs, models, answer terms;
• logical theories of interest for program verification, decision procedures, integration into existing ATP and SMT systems;
• combination of automated and user-assisted verification;
• tool presentations, tool comparisons, and benchmarks;
• experience reports on verification of complex algorithms and real-life software with the use of automated reasoning tools.

Invited speaker: K. Rustan M. Leino (Microsoft Research)

Abstract submission deadline: 8 March 2013
Camera ready versions due: 10 May 2013
Workshop: 10 June 2013

ESARAI, Empirically Successful Automated Reasoning with Artificial Intelligence

The Empirically Successful Automated Reasoning with Artificial Intelligence (ESARAI) workshop will bring together two complementary groups of researchers: researchers in Automated Reasoning who employ Artificial Intelligence tools and techniques to support their automated reasoning research, and researchers in Artificial Intelligence who employ Automated Reasoning tools and techniques to support the artificial intelligence research. The workshop will offer mutually beneficial interactions, through the exposure of the two sides of the research to all. Additionally, the workshop will provide a focused forum where the many interfaces between these two research fields can be presented and discussed. The workshop is soliciting research, position, applications and system description papers on combinations of AI and AR. Additionally, the workshop includes system and application demonstrations. Demonstrations of systems and applications described in paper presentations, and demonstrations of systems and applications without an accompanying paper, are both encouraged.

Notification of acceptance: 13 May 2013
Final versions due: 20 May 2013
Workshop: 9 or 10 June 2013

KInAR, Knowledge Intensive Automated Reasoning

Extensive digital sources of knowledge are becoming available, such as formal ontologies, databases, dictionaries and natural language reference works. Online sources like Wikipedia and IMDb, mathematical libraries like Mizar and various search engines and web services have gained widespread acceptance among the general population, but the sheer quantity of data can be an obstacle for human users. Automated reasoning (AR) systems have been advancing in their capabilities, and there is a growing interest in employing their deductive power to make digital knowledge more accessible. This poses challenges to AR research, but it is also a chance to bring AR into the public and to see large-scale usage of AR systems. In the KInAR workshop we aim to compile approaches to AR on large knowledge sources, and to aid the connections between researchers working on such projects.

We invite submissions on any topics regarding KInAR, such as:

• theoretical foundations: calculi for knowledge intensive reasoning,
• knowledge corpora and their management,
• extracting (semi-)formal knowledge from large informal corpora,
• system descriptions of applications regarding the workshop topic,
• benchmarking such systems,
• robustness: reasoning despite flaws in digital knowledge,
• combining knowledge from different sources.

KInAR workshop: 10 June 2013

M4M, Methods for Modalities

Detailed information is not yet available.

PxTP, Proof Exchange for Theorem Proving (PxTP)

The past decades have seen impressive advances in computer-aided reasoning, both in automated and interactive theorem proving. As shown by various system competitions, such as CASC, SMT-COMP, and the SAT competition, deduction tools are able to tackle larger problems progressively faster and are increasingly more applicable to a wider range of problems. In recent years, integration of such automated tools in larger verification environments has demonstrated the potential to reduce the amount of manual verification work.

It is becoming clear that the success of deduction tools will not only depend on their power to solve large and difficult problems in an isolated manner, but it will also rely on their ability to cooperate, by exchanging problems, proofs, and models. The PxTP workshop aims at encouraging such cooperation by inviting contributions on various aspects of communication, integration, and cooperation between systems and formalisms. The workshop's mission is to facilitate building of complex reasoning applications and reuse of reasoning tools by developing and discussing suitable integration, translation and communication methods, standards, protocols, and application programming interfaces (APIs). The workshop would like to bring together the interested developers of automatic and interactive theorem proving tools, developers of combined systems, developers and users of translation tools and APIs, and producers of standards and protocols.

Submission of papers: 11 April 2013
Camera-ready versions due: 9 May 2013
Workshop: 10 June 2013

StarExec Workshop

The StarExec project is an NSF funded project to design, implement, and operate StarExec, a web service designed for the comparative evaluation of logic solvers (automated theorem provers) on benchmark problems. The US\$1.85 million budget of the grant is mostly dedicated to purchasing and operating a medium-sized cluster of an anticipated 150 compute nodes, which will be used to run jobs submitted by users of the system. We anticipate users will be members of various logic-solving subcommunities of the broader automated theorem proving community

The StarExec 2013 workshop will bring together logic-solving community leaders, logic solver competition organizers, StarExec power users, and the StarExec organizers, to discuss the current status of the StarExec project. The workshop will have four sessions:

• A status report from the StarExec organizers, and a demonstration of StarExec as it has been developed by the time of the workshop.
• Use of StarExec by the attendees, so they can get a feeling of how well the implementation will meet their solver evaluation needs.
• A feedback session based on the use of StarExec.
• A presentation by the StarExec organisers on the short and medium terms plans for development and use of StarExec.

StarExec 2013 will not invite papers or general attendance. Rather, the workshop will be aimed specifically at the types of researchers described above, to maximise the positive impact on the development and use of StarExec. The NSF grant will provide travel, accommodation, and registration support for 20 participants, 10 from the USA and 10 from overseas.

SMT 2013, Satisfiability Modulo Therories

The 11th International Workshop on Satisfiability Modulo Theories, SMT 2013, will be held together with SAT 2013, in Helsinki, Finland, on 8–9 July 2013.

The aim of the workshop is to bring together researchers and users of SMT tools and techniques. Relevant topics include but are not limited to:

• Decision procedures and theories of interest
• Combinations of decision procedures
• Novel implementation techniques
• Benchmarks and evaluation methodologies
• Applications and case studies
• Theoretical results

Papers on pragmatic aspects of implementing and using SMT tools, as well as novel applications of SMT, are especially encouraged.

Papers may be submitted until 14 April 2013.

Please refer to the workshop website for further information.

Job opportunity: Post-doc in SAT/SMT-based Verification in Trento

One post-doc position in ICT on the research project “Advanced SMT Techniques for Word-level Formal Verification - (WOLF)” is available in Trento, Italy, under the joint supervision of Alessandro Cimatti, FBK, Trento, and Roberto Sebastiani, DISI, University of Trento.

The research activity will aim at investigating and developing novel techniques, methodologies and support tools for Satisfiability Modulo Theories (SMT) for the verification of WORD-level circuit designs. This work will be part of the "Word-Level Formal Verification via SMT Solving" (WOLFLING) project, a three-year custom research project supported by SRC/GRC, in strict collaboration with the Formal Verification Group at Intel, Haifa, Israel.