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.
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
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
Franz Baader, President of CADE Inc.
baader (at) tcs.inf.tu-dresden.de
with copies to
Martin Giese, Secretary of CADE Inc. and AAR
martingi (at) ifi.uio.no
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.
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 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.
At the time of writing, submission deadlines have not been fixed. For more information, please refer to the conference webs site.
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.
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
Full Paper submission: March 26, 2013
Notification: April 26, 2013
Final versions: May 10, 2013
Workshop: June 10, 2013
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:
Paper submission: 25 March 2013
Workshop: 9 June 2013
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:
Invited speaker: K. Rustan M. Leino (Microsoft Research)
Abstract submission deadline: 8 March 2013
Submission deadline: 15 March 2013
Notification: 10 April 2013
Camera ready versions due: 10 May 2013
Workshop: 10 June 2013
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.
Submission deadline: 22 April 2013
Notification of acceptance: 13 May 2013
Final versions due: 20 May 2013
Workshop: 9 or 10 June 2013
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:
Submission deadline: 8 April 2013
Author notification: 2 May 2013
Camera-ready version: 9 May 2013
KInAR workshop: 10 June 2013
Detailed information is not yet available.
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
Notification: 2 May 2013
Camera-ready versions due: 9 May 2013
Workshop: 10 June 2013
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:
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.
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:
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.
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.
See here for more information about this position.