# ASSOCIATION FOR AUTOMATED REASONING

## From the AAR President, Larry Wos…

I promised you some geometry, and here I fulfill that promise. I offer two theorems as challenges for you to prove.

That brilliant and versatile logician A. Tarski offered, at various times in his life, different axiom sets for plane geometry. In the following clauses, let `T` denote betweenness and `E` equidistance. Note that, for Tarski, `between' does not mean `strictly between.'

Given the axioms you are about to read, you are asked to prove two theorems. First, the five-point theorem: If point `a3` is between `a2` and `a4` and if each of `a2` and `a4` is between `a1` and `a5`, then `a3` is between `a1` and `a5`. Now, I think you will agree, the theorem seems more than believable. For the second theorem, the four-point theorem, thanks to Ross Overbeek: If each of `a3` and `a6` is between `a2` and `a4`, then `a3` is between `a2` and `a6` or `a6` is between `a2` and `a3`.

• identity axiom for betweenness:
```-T(x,y,x) | (x = y).
```
• transitivity axiom of betweenness:
```-T(x,y,u) | -T(y,z,u) | T(x,y,z).
```
• connectivity axiom for betweenness:
```-T(x,y,z) | -T(x,y,u) | (x = y) | T(x,z,u) | T(x,u,z).
```
• reflexivity axiom for equidistance:
```E(x,y,y,x).
```
• identity axiom for equidistance:
```-E(x,y,z,z) | (x = y).
```
• transitivity axiom for equidistance:
```-E(x,y,z,u) | -E(x,y,v,w) | E(z,u,v,w).
```
• Pasch's axiom (2 clauses):
```-T(x,v,u) | -T(y,u,z) | T(x,f1(v,x,y,z,u),y).
-T(x,v,u) | -T(y,u,z) | T(z,v,f1(v,x,y,z,u)).
```
• Euclid's axiom (three clauses):
```-T(x,u,v) | -T(y,u,z) | (x = u) | T(x,z,f2(v,x,y,z,u)).
-T(x,u,v) | -T(y,u,z) | (x = u) | T(x,y,f3(v,x,y,z,u)).
-T(x,u,v) | -T(y,u,z) | (x = u) | T(f2(v6,x,y,z,u),v6,f3(v6,x,y,z,u)).
```
• five-segment axiom:
```-E(x1,y1,x2,y2) | -E(y1,z1,y2,z2) | -E(x1,u1,x2,u2) | -E(y1,u1,y2,u2) | -T(x1,y1,z1) | -T(x2,y2,z2) | (x1 = y1) | E(z1,u1,z2,u2).
```
• axiom of segment construction (two clauses):
```T(x,y,f4(x,y,u,v)).
E(y,f4(x,y,u,v),u,v).
```
• lower dimension axiom (three clauses):
```-T(c1,c2,c3).
-T(c2,c3,c1).
-T(c3,c1,c2).
```
• upper dimension axiom:
```-E(x,u,x,v) | -E(y,u,y,v) | -E(z,u,z,v) | (u = v) | T(x,y,z) | T(y,z,x) | T(z,x,y).
```
• weakened continuity axiom (two clauses):
```-E(u1,x1,u1,x2) | -E(u1,z1,u1,z2) | -T(u1,x1,z1) | -T(x1,y1,z1) | E(u1,y1,u1,f5(x1,y1,z1,x2,z2,u1)).
-E(u1,x1,u1,x2) | -E(u1,z1,u1,z2) | -T(u1,x1,z1) | -T(x1,y1,z1) | T(x2,f5(x1,y1,z1,x2,z2,u1),z2).
```

I did not include here the axioms regarding equality. If you wish to see these, with a slightly different notation, I recommend Chapter 6 of a book I wrote in 1987, 33 Basic Research Problems.

## Automated Reasoning in the ACM Computing Classification System

Maria Paola Bonacina
E-mail: mariapaola.bonacina (at) univr.it

On March 30, 2012, the Association for Computing Machinery released the 2012 Revision of its Computing Classification System (CCS), available online here, that will be used in ACM journals beginning January 2013. I browsed the new CCS, being curious to see where our field appears. I remembered that the previous version mentioned keywords broadly related to our field in at least three places:

• ```Theory of Computation
Mathematical Logic and Formal Languages
Mathematical Logic
Mechanical Theorem Proving
```
• ```Theory of Computation
Mathematical Logic and Formal Languages
Grammars and Other Rewriting Systems
Decision Problems
```
• ```Computing Methodologies
Artificial Intelligence
Deduction and Theorem Proving
Inference Engines, Resolution
```

In the new taxonomy I could find:

• ```Hardware
Hardware validation
Functional verification
Theorem proving and SAT solving
```
• ```Theory of computation
Formal languages and automata theory
Formalisms
Rewrite systems
```
• ```Theory of computation
Logic
Automated reasoning
```
• ```Theory of computation
Logic
Equational logic and rewriting
```
• ```Computing methodologies
Symbolic and algebraic manipulation
Symbolic and algebraic algorithms
Theorem proving algorithms
```
• ```Computing methodologies
Artificial intelligence
Knowledge representation and reasoning
Description Logics
Nonmonotonic, default reasoning and belief revision
Probabilistic reasoning
Causal reasoning and diagnostics
Temporal reasoning
Ontology engineering
Logic programming and answer set programming
Spatial and physical reasoning
```

Thus, there are many improvements: there are more entries related to our field; `Automated reasoning` shows up explicitly; the relevance of `Theorem proving and SAT solving` to hardware verification is openly recognized; the fact that our field has evolved into an increasingly algorithmic field is acknowledged with `Theorem proving algorithms`.

On the other hand, there is no mention of theorem proving or other automated reasoning keywords under `Software and its engineering`, notwithstanding the growth of reasoning based technologies for program checking and analysis.

Also, the historic connection of our field with `Artificial intelligence` appears significantly weakened, since `Automated reasoning` is squarely under `Logic`, and therefore under `Theory of computation`, while under `Artificial intelligence` remains `Knowledge representation and reasoning`. An explanation suggesting that it is so, because automated reasoning has its own conferences, independent of AI conferences since decades, does not persuade, because `Computer vision`, whose conferences are as independent of AI as automated reasoning conferences, is still fully under `Artificial intelligence`. Perhaps, the view of artificial intelligence as heuristic reasoning and perception has prevailed over the view of artificial intelligence as formal reasoning. Symmetrically, the view of automated reasoning as mechanized logic has prevailed over the consideration that automated reasoning also means heuristic and search.

A classification of a multi-faceted discipline like computer science is a daunting task, and the effort of all the scientists who worked on the CCS has to be acknowledged and thanked for. However, while the previous system was probably less sophisticated, the presence of `Mechanical Theorem Proving` under `Logic`, and `Deduction and Theorem Proving` under `Artificial intelligence`, acknowledged the composite nature of our field, its having mixed roots in theory, logic and AI. As the Alan Turing Centenary celebrations of this year made these intertwined roots feel as strong as ever, the neat separation of the new taxonomy might satisfy the quest for clarity and lack of redundancy more than that for long-term, deep, cross-fertilizing connections.

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

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

### TABLEAUX 2013, Automated Reasoning with Analytic Tableaux and Related Methods

This conference is the 22nd in a series of international meetings on Automated Reasoning with Analytic Tableaux and Related Methods and will be held in Nancy, France, on 16–19 September 2013.

Tableaux methods offer a convenient set of formalisms for automating deduction in various non-standard logics as well as in classical logic. Areas of application include verification of software and computer systems, data integration and data access, deductive databases, knowledge representation and its required inference engines, and system diagnosis.

The conference intends to bring together researchers interested in all aspects – theoretical foundations, implementation techniques, system developments and applications – of the mechanization of reasoning with tableaux and related methods.

TABLEAUX 2013 will be co-located with the 9th International Symposium on Frontiers of Combining Systems (FroCos 2013) held 18–20 September 2013.

The submission deadlines are as follows: Workshop proposals: 22 February 2013, notification 8 March. Tutorials: 23 March 2013, notification 5 April. Research papers: abstracts on 8 April, full papers on 15 April.

Further information is available at the conference web site.

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

### CAV 2013, Computer Aided Verification

The 25th International Conference on Computer Aided Verification (CAV 2013) will be held in St. Petersburg, Russia, on 13–19 July 2013. The CAV conference series is dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems.

Amongst many other topics, deduction techniques for hardware and software verification lie within the scope of the conference. CAV 2013 will have special tracks on Hardware Verification, Computer Security, SAT and SMT, and Biology.

The paper submission deadline is 7 January, with abstracts to be submitted until 3 January 2013.

Please refer to the CAV 2013 web site for further details.

### TAP 2013, Tests and Proofs

The 7th International Conference on Tests and Proofs, TAP 2013, will take place in Budapest, Hungary, om 17–21 June, 2013.

The TAP conference is devoted to the synergy of proofs and tests, to the application of techniques from both sides and their combination for the advancement of software quality.

Research papers of up to 16 pages, and short papers of up to 6 pages should be submitted until 1 February, abstracts are due on 25 January 2013.

## Science of Computer Programming – Special Issue on Invariant Generation

This special issue is devoted to the 4th international Workshop on Invariant Generation (WING 2012) which was held on 30 June 2012 in Manchester as a satellite event of IJCAR 2012. The scope of the workshop is the automation of extracting and synthesising auxiliary properties of programs, in particular providing, debugging, and verifying auxiliary invariant annotations. This should be seen in a broad sense and relevant topics include (but are not limited to) the following:

• Program analysis and verification
• Inductive assertion generation
• Inductive proofs for reasoning about loops
• Applications to assertion generation using:
• abstract interpretation,
• static analysis,
• model checking,
• theorem proving,
• theory formation,
• algebraic techniques
• Tools for inductive assertion generation and verification
• Alternative techniques for reasoning about loops

Submission to this special issue is completely open. We expect original articles (typically not more than 30 pages) that present high-quality contributions and must not be simultaneously submitted for publication elsewhere. Submission of extended versions of previously published papers is possible as long as the extension is significant, i.e., the submission can be considered a new paper, the previous paper is referenced, and the new material is clearly marked.

Submissions must comply with SCP's author guidelines and be written in English. Submission is over the SCP website, which you will have to register for if you do not have an account. When submitting your paper, please choose the article type “Special issue: WING 2012”.

Papers should be submitted until 11 February 2013, and authors will be notified on 26 April 2013. Please send any queries you may have to `wing2012 (at) easychair.org`

## Job Opportunity in Automated Reasoning

IPSNP Computing Inc is looking for an Automated Reasoning Engineer to play a key role in the development of a new technology for Biomedical Data Federation.

• Development of a specialised reasoning engine as a core component of IPSNP's query engine for SADI Semantic Web services.
• Design and implementation of other components of the query engine, related to the processing of RDF, OWL and SPARQL, and one or more rule languages.
• Design and implementation of other components of the query engine, related to the discovery and invocation of SADI services.

The following qualifications are mandatory:

• Research experience in an area related to Automated Reasoning implementation.
• PhD or MSc with work experience in relevant fields.
• Good knowledge of the Java programming language.

The following will be considered an advantage:

• Experience with Semantic Technologies (RDF, OWL, SPARQL).
• Familiarity with rule-based reasoning.
• Experience with Web service technologies, client-side or server-side, especially experience with Semantic Web services and/or the use of Web services for data integration.
• Experience with any data integration technologies.
• Experience in Natural Language Processing.
• Industrial software development work experience.
• Any exposure to Bioinformatics.

This job will be located in Saint John, New Brunswick, Canada.

The position is open until filled. We encourage international applicants to complete the application process as early as possible due to the length of time required to obtain a Canadian work permit.

Interested applicants are invited to write to Dr. Chris Baker (chris.baker (at) ipsnp.com). Enquiries about the job should be directed to Dr. Alexandre Riazanov (alexandre.riazanov (at) ipsnp.com).