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.
-T(x,y,x) | (x = y).
-T(x,y,u) | -T(y,z,u) | T(x,y,z).
-T(x,y,z) | -T(x,y,u) | (x = y) | T(x,z,u) | T(x,u,z).
E(x,y,y,x).
-E(x,y,z,z) | (x = y).
-E(x,y,z,u) | -E(x,y,v,w) | E(z,u,v,w).
-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)).
-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)).
-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).
T(x,y,f4(x,y,u,v)). E(y,f4(x,y,u,v),u,v).
-T(c1,c2,c3). -T(c2,c3,c1). -T(c3,c1,c2).
-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).
-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.
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
Reasoning about belief and knowledge
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.
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:
Paradigms of interest include:
Methods of interest include:
Applications of interest include:
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.
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, 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.
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.
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.
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:
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
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.
The main tasks will be:
The following qualifications are mandatory:
The following will be considered an advantage:
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).