# ASSOCIATION FOR AUTOMATED REASONING

## From the AAR President, Larry Wos…

Occasionally in mathematics and in logic, the goal is not only to find a proof but also to find a proof with some constraint.

For example, you might be asked to find a proof from a set of axioms all of which are independent, as in group theory when the axioms of right identity and right inverse are omitted. For a second example, you might be asked, as I was by Branden Fitelson, to find for a particular theorem, a proof that avoided various lemmas that are usually present in the literature. For a third example, pertinent to this column, you are asked first to find a proof under no constraints, and then under the constraint that certain terms are avoided. The terms to be avoided are so-called double-negation terms, terms of the form `n(n(t))` for some term `t`, where the function `n` denotes negation. The area in focus is many-valued, or infinite-valued, sentential calculus. The inference rule is condensed detachment.

I now give a set of three lists – `usable`, `sos`, and `passive` – all pertinent to William McCune's program OTTER. Condensed detachment is found in `list(usable)`, the axioms to be used are found in `list(sos)`, and the target theorems are found, negated, in `list(passive)`.

The key theorem to concentrate on is 44a.

You are asked first to find a proof of that theorem under no constraints, and then – more challenging indeed – under the constraint that no double-negation term is used.

```   list(usable).
-P(i(x,y)) | -P(x) | P(y).
end_of_list.

list(sos).
P(i(x,i(y,x))).                   % A1
P(i(i(x,y),i(i(y,z),i(x,z)))).    % A2
P(i(i(i(x,y),y),i(i(y,x),x))).    % A3
P(i(i(n(x),n(y)),i(y,x))).        % A4
end_of_list.

list(passive).
-P(i(i(a,b),i(n(b),n(a)))) | \$ANS(mv_lemma_a6).
-P(i(i(n(a),b),i(n(b),a))) | \$ANS(mv_lemma_a7).
-P(i(i(a,n(b)),i(b,n(a)))) | \$ANS(mv_lemma_a8).
-P(i(i(a,n(i(i(n(b),n(c)),n(c)))),n(i(i(n(i(a,b)),n(i(a,c))),n(i(a,c)))))) | \$ANS(step_dist_44a).
end_of_list.
```

Franz Baader's term as CADE trustee expired after the trustee elections 2013, and with that ended his office as president. The new Board of Trustees has elected Maria Paola Bonacina as new president of CADE.

On the behalf of CADE and AAR, I congratulate Maria Paola Bonacina on this honor and opportunity to serve CADE and the field of automated reasoning.

Also on behalf of the AAR and CADE, I would like to thank Franz Baader for his service and commitment as president of CADE during the past three years.

## Conferences

### FLoC 2014, Federated Logic Conference, Call for Workshop Proposals

The Sixth Federated Logic Conference (FLoC 2014) will be part of the Vienna Summer of Logic (VSL), the largest logic event in history, with over 2000 expected participants. FLoC 2014 will host eight conferences and many workshops. Each workshop will be affiliated with one of the eight conferences.

• 26th International Conference on Computer Aided Verification (CAV)
Workshop Chair: Martina Seidl
• 27th IEEE Computer Security Foundations Symposium (CSF)
Workshop Chair: Luca Vigano
• 30th International Conference on Logic Programming (ICLP)
Workshop Chair: Haifeng Guo
• 7th International Joint Conference on Automated Reasoning (IJCAR)
Workshop Chair: Matthias Horbach
• 5th Conference on Interactive Theorem Proving (ITP)
Workshop Chair: David Pichardie
• 29th ACM/IEEE Symposium on Logic in Computer Science (LICS) joined with the 23rd EACSL Annual Conference on Computer Science Logic (CSL)
Workshop Chair: Georg Moser
• 25th International Conference on Rewriting Techniques and Applications (RTA) joined with the 12th International Conference on Typed Lambda Calculi and Applications (TLCA)
Workshop Chair: Aleksy Schubert
• 17th International Conference on Theory and Applications of Satisfiability Testing (SAT)
Workshop Chair: Ines Lynce

Researchers and practitioners are invited to submit proposals for workshops on topics in the field of computer science, related to logic in the broad sense. Each workshop proposal must indicate one hosting conference among the participating conferences.

It is suggested that prospective workshop organizers contact the relevant conference Workshop Chair before submitting a proposal. Proposals should be submitted electronically to EasyChair.

The deadline for workshop proposals is 30 September 2013.

Questions regarding workshop proposals should be sent to the workshop chairs of conferences that are supposed to host the workshop (see above). General questions should be sent to floc14cfw@easychair.org. For full details, please refer to the FLoC Workshop Guide.

### LPAR-19, Logic for Programming Artificial Intelligence and Reasoning

The 19th edition of the International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-19) will be held in Stellenbosch, South Africa, 14–19 December 2013. LPAR-19 includes five associated workshops:

• IWIL-10 - The 10th International Workshop on the Implementation of Logics, Submission deadline: October 14, 2013
• APS-7 - The 7th International Workshop on Analytic Proof Systems, Submission deadline: October 14, 2013
• ALCS - The 1st International Workshop on Algebraic Logic in Computer Science, Submission deadline: passed
• LRCM - The 1st Workshop on Logics and Reasoning for Conceptual Models, Submission deadline: October 14, 2013
• ALFA-2 - The 2nd Workshop on Automata, Logic, Formal languages, and Algebra, Submission deadline: September 30

Submissions are still being accepted for most workshops. For further details, please refer to the workshop web pages.

### FMCAD 2013, Formal Methods in Computer-Aided Design

FMCAD 2013 will be held in Portland, Oregon, USA on 20–23 October 2013. The conference will be co-located with MEMOCODE 2013, the ACM/IEEE International Conference on Formal Methods and Models for Codesign, and DIFTS 2013, the International Workshop on Design and Implementation of Formal Tools and Systems. DIFTS will be held on October 19. 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.

Early registration will be open until 30 September 2013. Please refer to the conference webs site for details.

### LATA 2014, Language and Automata Theory and Applications

LATA 2014, the 8th Intl. Conf. on Language and Automata Theory and Applications will be held in Madrid, Spain on 10–14 March 2014.Topics of either theoretical or applied interest include connections between automata and logic, term rewriting, and others that may be of interest to the AAR community.

The paper submission deadline is 14 October 2013. Accepted papers will be published in a Springer LNCS volume.

Please go to the conference web site for details.

### FM 2014, International Symposium on Formal Methods

FM 2014, the 19th International Symposium on Formal Methods will take place in Singapore on 14–16 May 2014. This series of symposia is organized by
Formal Methods Europe, an independent association whose aim is to stimulate the use of, and research on, formal methods for software development.

Topics of interest include theory and tools for specification, verification, model checking, refinement, etc.

Accepted papers will be published in Springer's LNCS series. Abstracts are due on 7 November 2013, and full papers on 14 November.

For details, please refer to the Symposium web page

### NFM 2014, NASA Formal Methods Symposium

The sixth NASA Formal Methods Symposium will take place at the NASA Johnson Space Center at Houston, Texas, USA, from 29 April to 1 May 2014. NFM is a forum for theoreticians and practitioners from academia and industry, with the goals of identifying challenges and providing solutions to achieving assurance in 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. Submissions on cross-cutting approaches are encouraged, marrying formal verification techniques with advances in safety-critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages carrying throughout system development.

Accepted papers will appear as a Springer LNCS volume. Abstracts should be submitted until 14 November 2013, with full papers of 15 pages, or short papers of 6 pages until 21 November. For full details, refer to the symposium web site.

## Job Opportunities

### Post-doc Position in Trento, Italy

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

The research activity will be carried out jointly within the Embedded Systems (ES) Research Unit of the Center for Scientific and Technological Research of the Fondazione Bruno Kessler (FBK), Trento, and the Software Engineering & Formal Methods (SE&FM) Research Program, at Department of Information Engineering and Computer Science (DISI) of 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 formal verification of systems. This work will be part of the "Advanced SMT Techniques for Word-level Formal Verification –(WOLF)" project, a three-year research project supported by SRC/GRC, in collaboration with major HW companies.

The ultimate goal of the WOLF project is to provide a comprehensive SMT package to support effective formal verification of systems ranging from RTL circuits all the way up to high-level hardware description languages (e.g. SystemC) and software. The package will be implemented on top of the MathSAT SMT platform, and provided as an API.

The ideal candidate should have an PhD in computer science or related discipline, and combine solid theoretical background and excellent software development skills (in particular C/C++).

A solid background knowledge and/or previous experience on one of the following topics (in order of preference) is required: Satisfiability Modulo Theory (SMT), Propositional Satisfiability (SAT), Model Checking, Automated Reasoning. Previous experience in the following areas will also be considered favourably: Constraint Solving and Optimization, Embedded Systems Design Languages (e.g. Verilog, VHDL).

The candidate should be able to work in a collaborative environment, with a strong committment to reaching research excellence and achieving assigned objectives.

Early availability will be considered with much favour.

Interested candidates should inquire for further information and/or apply by sending email to wolf-recruit (at) disi.unitn.it

Applications should contain a statement of interest, with a Curriculum Vitae, and the names of reference persons. PDF format is strongly encouraged. It should also indicate an estimated starting date.

Emails will be automatically processed and should have 'PHD ON WOLF PROJECT' as subject.

Contact Persons: Prof. ROBERTO SEBASTIANI (rseba[at]disi[dot]unitn[dot]it), Dr. ALESSANDRO CIMATTI (cimatti [at] fbk [dot] eu)

## Results of CADE Trustee Elections

Martin Giese
E-mail: martingi (at) ifi.uio.no

An election was held from 24 July to 20 August to fill four positions on the board of trustees of Cade, Inc. Peter Baumgartner, Maria Paola Bonacina, Christopher Lynch, Larry Paulson, Brigitte Pientka, and Carsten Schuermann were nominated.

Ballots were sent by electronic mail to all members of AAR on 24 July, for a total of 1038 ballots. 123 valid ballots were returned, which translates to a participation level of 11.8% (as compared to 13,0% in 2012, 16.2% in 2011, 13.3% in 2010, 18.3% in 2009, 18% in 2008, and 16.4% in 2007).

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 62 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. Peter Baumgartner 33 27 20 14 14 8 7 Maria Paola Bonacina 25 31 16 14 10 7 20 Christopher Lynch 13 11 21 16 22 18 22 Larry Paulson 32 18 16 17 17 11 12 Brigitte Pientka 8 20 25 21 18 12 19 Carsten Schuermann 12 13 19 23 13 25 18

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Brigitte Pientka, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. no supp. Peter Baumgartner 33 34 21 17 11 7 Maria Paola Bonacina 25 36 20 15 7 20 Christopher Lynch 14 13 26 25 23 22 Larry Paulson 36 17 18 26 14 12 Carsten Schuermann 15 20 25 18 27 18

No candidate reaches at least 62 first preference votes.

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

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. no supp. Peter Baumgartner 38 36 28 14 7 Maria Paola Bonacina 33 33 23 14 20 Larry Paulson 36 24 29 22 12 Carsten Schuermann 16 26 27 36 18

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Carsten Schuermann, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. no supp. Peter Baumgartner 42 52 22 7 Maria Paola Bonacina 38 39 26 20 Larry Paulson 43 23 45 12

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Maria Paola Bonacina, one gets the following table:

 Candidate 1st pref. 2nd pref. no supp. Peter Baumgartner 71 45 7 Larry Paulson 52 59 12

Now, Peter Baumgartner reaches at least 62 first preference votes, and is elected.

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

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. no supp. Maria Paola Bonacina 38 32 13 9 11 20 Christopher Lynch 17 19 19 25 21 22 Larry Paulson 39 21 20 20 11 12 Brigitte Pientka 14 28 28 22 12 19 Carsten Schuermann 14 18 29 18 26 18

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Carsten Schuermann, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. no supp. Maria Paola Bonacina 42 35 14 12 20 Christopher Lynch 19 22 34 26 22 Larry Paulson 43 24 26 18 12 Brigitte Pientka 18 33 26 27 19

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Brigitte Pientka, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. no supp. Maria Paola Bonacina 48 42 13 20 Christopher Lynch 22 37 42 22 Larry Paulson 51 27 33 12

No candidate reaches at least 62 first preference votes.

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

 Candidate 1st pref. 2nd pref. no supp. Maria Paola Bonacina 63 40 20 Larry Paulson 57 54 12

Now, Maria Paola Bonacina reaches at least 62 first preference votes, and is elected.

To find the next elected candidate, we redistribute the votes of Maria Paola Bonacina and get the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. no supp. Christopher Lynch 33 15 24 29 22 Larry Paulson 49 26 23 13 12 Brigitte Pientka 22 40 28 14 19 Carsten Schuermann 18 32 26 29 18

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Carsten Schuermann, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. no supp. Christopher Lynch 36 28 37 22 Larry Paulson 55 36 20 12 Brigitte Pientka 29 44 31 19

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Brigitte Pientka, one gets the following table:

 Candidate 1st pref. 2nd pref. no supp. Christopher Lynch 46 55 22 Larry Paulson 72 39 12

Now, Larry Paulson reaches at least 62 first preference votes, and is elected.

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

 Candidate 1st pref. 2nd pref. 3rd pref. no supp. Christopher Lynch 43 21 37 22 Brigitte Pientka 44 42 18 19 Carsten Schuermann 31 39 35 18

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Carsten Schuermann, one gets the following table:

 Candidate 1st pref. 2nd pref. no supp. Christopher Lynch 54 47 22 Brigitte Pientka 58 46 19

No candidate reaches at least 62 first preference votes.

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

 Candidate 1st pref. no supp. Brigitte Pientka 104 19

Now, Brigitte Pientka reaches at least 62 first preference votes, and is elected.

To summarize, the 4 candidates elected are Peter Baumgartner, Maria Paola Bonacina, Larry Paulson, and Brigitte Pientka.

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

• Peter Baumgartner (elected 2013)
• Maria Paola Bonacina (elected 2013, president)
• Martin Giese (secretary)
• Bernhard Gramlich (elected 2012)
• Deepak Kapur (IJCAR 2014 program co-chair)
• Neil Murray (treasurer)
• Larry Paulson (reelected 2013)
• Brigitte Pientka (reelected 2013)
• Renate Schmidt (reelected 2012, vice-president)
• Viorica Sofronie-Stokkermans (elected 2011)
• Geoff Sutcliffe (elected 2011)
• Christoph Weidenbach (reelected 2012)

On behalf of the AAR and CADE Inc., I thank Franz Baader for three years of service as member and president of the CADE Board of Trustees. We are also grateful to Amy Felty, who has been a member of the Board for six years.

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

Congratulations to Peter Baumgartner, Maria Paola Bonacina, Larry Paulson, and Brigitte Pientka on being elected!