ASSOCIATION FOR AUTOMATED REASONING

From the AAR President, Larry Wos…

Algebra is in focus in this column; geometry will most likely again follow soon.

As noted in an earlier column, 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.

I give you the following problem, from ring theory, to address.

Let a and b be elements of a ring such that a, b, and ab − 1 are units.
Show that ab-1 is unit.

In OTTER notation, the hypotehsis and denial of conclusion are the following.

```  a * inv(a) = 1.
b * inv(b) = 1.
(a*b + m(1)) * inv(a*b + m(1)) = 1.
%  negated goal
(a + m(inv(b))) * x != 1.

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

You are first challenged to find a proof, any proof.

Then, perhaps more challenging, you are asked to find a forward proof.

Greg Nelson to receive Herbrand Award

International Conference on Automated Deduction (CADE)
Herbrand Award for Distinguished Contributions to Automated Reasoning
presented to

Greg Nelson

for his pioneering contributions to theorem proving and program verification, such as his seminal work with Derek Oppen on the combination of satisfiability procedures and fast congruence closure algorithms, the development of the highly influential theorem prover Simplify, and his role in the creation of the field of extended static checking.

The Award will be presented at CADE 24, the 24th International Conference on Automated Deduction.

CADE-24: Woody Bledsoe Student Travel Award

Maria Paola Bonacina

The Woody Bledsoe Student Travel Award was created to honor the memory of Woody Bledsoe, for his contributions to mathematics, artificial intelligence, and automated theorem proving, and for his dedication to students. The award is intended to enable selected students to attend the International Conference on Automated Deduction (CADE) or the International Joint Conference on Automated Reasoning (IJCAR), whichever is scheduled for the year, by covering part of their expenses.

In 2013, CADE will take place from June 9 through June 14, in Lake Placid, New York, USA (for further information see the CADE web page). The winners will be partially reimbursed (e.g., between USD 200 and USD 750) for their conference registration, transportation, and accomodation expenses. Preference will be given to students who will play an active role in the conference, including satellite workshops, and do not have alternative funding. However, also students in other situations are very much encouraged to apply.

A nomination consists of a recommendation letter of up to 300 words from the student’s advisor. Nominations for CADE-24 should be sent by e-mail to

Maria Paola Bonacina, CADE-24 Program Chair (mariapaola.bonacina (at) univr.it)

and

Christopher A. Lynch and Neil V. Murray, CADE-24 Conference Chairs (clynch (at) clarkson.edu and nvm (at) cs.albany.edu)

Nominations must arrive no later than May 2, 2013. The selection will be made by the Chairs together with the Program Committee and the winners will be notified by May 9, 2013.

The awards will be presented at CADE-24; in case a winner does not attend, the chairs may transfer the award to another nominee or give no award.

Conferences

CADE 24, Conference on Automated Deduction, Call for Participation

The 24th International Conference on Automated Deduction will take place in Lake Placid, NY, USA, on 9–14 June 2013.

The deadline for early registration is 22 May 2013.

CADE is the major forum for the presentation of research in all aspects of automated deduction. CADE-24 is held in Lake Placid, a charming village on the shore of two lakes surrounded by the beautiful Adirondacks Mountains, upstate New York.

The conference program features:

• Invited talks:
• Jean-Christophe Filliatre: One Logic to Use Them All
• Greg Morrisett: Defining, Testing, and Reasoning About an x86 Decoder
• Natarajan Shankar: Automated Reasoning, Fast and Slow
• Douglas R. Smith: Coalgebraic Specification and Refinement
• Presentation of 31 papers including the CADE-24 Best Paper Award winner
• Tutorials:
• Franz Baader: Reasoning in Lightweight Description Logics
• Bernhard Beckert: Program Verification with the KeY System
• Morgan Deters, Dejan Jovanovic, Clark Barrett and Cesare Tinelli: Becoming a Power User of SMT: The CVC4 Solver
• Marijn Heule: State-of-the-art SAT Solving
• Carsten Schuermann, Taus Brock-Nannestad and Chris Martens: Twelf
• Several Workshops
• The CADE ATP System Competition (CASC)
• During the conference, the Herbrand Award for Distinguished Contributions to Automated Reasoning will be presented to Greg Nelson for his invention of equality sharing, also known as the Nelson-Oppen method, and his pioneering work on theorem proving and program checking, including fast congruence closure algorithms and the Simplify theorem prover.

IMPORTANT DATES:

Early registration deadline: 22 May 2013
Workshops and Tutorials: 9-10 June 2013
Conference: 11-14 June 2013
CASC: 12 June 2013

Please refer to the conference web site for further information.

FroCoS 2013, Frontiers of Combining Systems

FroCoS 2013, the 9th International Symposium on Frontiers of Combining Systems will take place in Nancy, France, on 18–20 September 2013. FroCos will be co-located with TABLEAUX 2013, the 22nd conference on AR with Analytic Tableaux and Related methods.

In various areas of computer science, such as logic, computation, program development and verification, artificial intelligence, knowledge representation and automated reasoning, there is an obvious need for using specialised formalisms and inference mechanisms for special tasks. In order to be usable in practice, these specialised systems must be combined with each other, and they must be integrated into general purpose systems.

Like its predecessors, FroCoS 2013 seeks to offer a common forum for research in the general area of combination, modularization and integration of systems, with emphasis on logic-based ones, and of their practical use.

Research papers of up to 16 pages are to be submitted until 22 April 2013, with abstracts due on 15 April. Please refer to the conference web site for full details, including submission information.

LPAR-19, Logic for Programming, Artificial Intelligence and Reasoning: Call for Papers and Workshops

LPAR-19, the 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning will take place in Stellenbosch, South Africa, 14–19 December 2013. New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to:

 Abduction and interpolation methods Automated reasoning Constraint programming Decision procedures Description logics Foundations of security Hardware verification Implementations of logic Interactive theorem proving Knowledge representation and reasoning Logic and computational complexity Logic and databases Logic and games Logic and machine learning Logic and the web Logic and types Logic in artificial intelligence Logic of distributed systems Logic programming Logical aspects of concurrency Logical foundations of programming Modal and temporal logics Model checking Non-monotonic reasoning Ontologies and large knowledge bases Probabilistic and fuzzy reasoning Program analysis Rewriting Satisfiability checking Satisfiability modulo theories Software verification Specification using logic Unification theory

The deadline for paper submission is 2 August, with abstracts due on 22 July.

LPAR-19 also calls for workshop proposals. Workshops will be held on 14th December either as one-day or half-day events. If you would like to propose a workshop for LPAR-19, please contact the workshop chair via email (lkovacs (at) complang.tuwien.ac.at), until 15 July.

TYPES 2013, Types for Proofs and Programs, Call for Participation

The 19th Meeting on Types for Proofs and Programs will take place in Toulouse, France on 22–26 April 2013.

The Types Meeting is a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalized and computer assisted reasoning and computer programming.

Invited Speakers:

• Steve Awodey (Institute for Advanced Study, Princeton & Carnegie
Mellon University, Pittsburgh): “Higher Inductive Types in Homotopy Type Theory”
• Lars Birkedal (Aarhus University):
“Charge! a framework for higher-order separation logic in Coq.”
• Ulrich Kohlenbach (Technische Universitaet Darmstadt):
“Types in Proof Mining”

34 contributed talks were selected by the program committee (main conference: morning of April 23 to midday of April 26).

Satellite events:

• Twelfth international workshop Proof, Computation, Complexity (PCC 2013) with 12 selected contributed talks on 22–23 April
• tutorial on separation logic by Lars Birkedal in the late afternoon of April 22: “An introduction to separation logic, and the benefits of going higher-order”
• Workshop CSPM “Computer Science, Philosophy, Mathematics” in the afternoon of April 26

All the details are accessible through the main web site of TYPES 2013.

Workshops

SYNASC 2013, Symbolic and Numeric Algorithms for Scientific Computing

The 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2013)
will take place in Timisoara, Romania, on 23–26 September 2013.

SYNASC aims to stimulate the interaction between the two scientific communities of symbolic and numeric computing and to exhibit interesting applications of the areas both in theory and in practice. Symbolic computing is here taken in a broad sense, to include computational logic, theorem proving, formal verification, etc. The choice of the topic is motivated by the belief of the organizers that the dialogue between the two communities is very necessary for accelerating the progress in making the computer a truly intelligent aid for mathematicians and engineers.

Proposals for Workshops, Tutorials, and Special Sessions are invited until 7 April 2013. Research papers are to be submitted until 26 May 2013, with abstracts due on 19 May.

Please refer to the Symposium Web Page for further details.

Job Opportunities

PhD Positions and Fellowships at RISC, Hagenberg, Austria

The Research Institute for Symbolic Computation (RISC) offers positions and fellowships for doctoral studies in symbolic computation.

The Research Institute for Symbolic Computation (RISC) in the castle of Hagenberg, Austria, is an international institute with its research focus on various branches of symbolic computation. Research interests of RISC include

• Algebraic Geometry
• Algorithmic Combinatorics
• Automated Reasoning
• Computer Algebra
• Parallel and Distributed Computing
• Scientific Computing

RISC seeks applications of excellent and highly motivated students with a university degree in mathematics and/or computer science. Experience in symbolic computation is an advantage but no formal requirement.

More information is available from the web site of the PhD programme.

Doctoral Student Positions in Trento, Italy

Doctoral Student Positions in Information and Communication Technologies on the research project “Advanced SMT Techniques for Word-level Formal Verification - (WOLF)” are available at the International Doctorate School in Information and Communication Technologies of 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 strict collaboration with the Formal Verification Group at Intel, Haifa, and other major HW companies.

The 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.5 SMT platform (http://mathsat.fbk.eu/), and provided as an API.

Ph.D. courses will start in Autumn 2013, and the thesis must be completed in three or four years. People enrolled Ph.D. courses are expected to move to Trento, and will receive monetary support during phases of their activity.

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 three reference persons. PDF format is strongly encouraged.

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

Contact Person: Prof. ROBERTO SEBASTIANI (rseba[at]disi[dot]unitn[dot]it)

E. W. Beth Dissertation Prize: 2013 call for nominations

Since 2002, FoLLI (the Association for Logic, Language, and Information, ) awards the E.W. Beth Dissertation Prizeto outstanding dissertations in the fields of Logic, Language, and Information. We invite submissions for the best dissertation which resulted in a Ph.D. degree in the year 2012. The dissertations will be judged on technical depth and strength, originality, and impact made in at least two of three fields of Logic, Language, and Computation. Interdisciplinarity is an impor tant feature of the theses competing for the E.W. Beth Dissertation Prize.

Who qualifies. Nominations of candidates are admitted who were awarded a Ph.D. degree in the areas of Logic, Language, or Information between January 1st, 2012 and December 31st, 2012. There is no restriction on the nationality of the candidate or the university where the Ph.D. was granted. After a careful consideration, FoLLI has decided to accept only dissertations written in English. Dissertations produced in 2012 but not written in English or not translated will be allowed for submission, after translation, also with the call next year (for dissertations defended in 2013). The present call for nominations for the E.W. Beth Disertation Award 2013 will also accept nominations of full English translations of theses originally written in another language than English and defended in 2011 or 2012.

The prize consists of:

• a certificate
• a donation of 2500 euros provided by the E.W. Beth Foundation
• an invitation to submit the thesis (or a revised version of it) to the FoLLI Publications on Logic, Language and Information (Springer). For further information on this series see the FoLLI site.

How to submit. Only electronic submissions are accepted. The following documents are required:

1. The thesis in pdf format (ps/doc/rtf not accepted);
2. A ten page abstract of the dissertation in pdf format;
3. A letter of nomination from the thesis supervisor. Self-nominations are not admitted: each nomination must be sponsored by the thesis supervisor. The letter of nomination should concisely describe the scope and significance of the dissertation and state when the degree was officially awarded;
4. Two additional letters of support, including at least one letter from a referee not affiliated with the academic institution that awarded the Ph.D. degree.

All documents must be submitted electronically (preferably as a zip file) to buszko (at) amu.edu.pl. Hard copy submissions are not admitted. In case of any problems with the email submission or a lack of notification within three working days, nominators should write to buszko (at) amu.edu.pl.

Important dates:

Deadline for Submissions: May 12, 2013.
Notification of Decision: July 14, 2013.

Book announcement: Mutually-inversistic logic, mathematics, and their applications

Xunwei Zhou

Mutually-inversistic logic deems that the truth table for material implication cannot be used to make hypothetical inference but its inverse functions can. Mutually-inversistic logic includes two calculi and four theories.

Mutually-inversistic mathematics includes algebra, geometry, and analysis.

In rule-based systems, a rule is both an inference rule and a tautology. In mutually-inversistic automated decomposition systems, a rule is either an inference rule or a tautology but not both, especially hypothetical syllogism is a tautology but not an inference rule. In this way, reasoning can be made automated. Mutually-inversistic automated decomposition systems include an automated theorem prover for hardware verification and mutually-inversistic program verification.

My monograph entitled “Mutually-inversistic logic, mathematics, and their applications” has been published by Central Compilation & Translation Press. It contains a discussion of automated reasoning for mutually-inversistic logic.