Many programs now exist that can attempt to find proofs of theorems
in various fields. As so many of you know, my favorite program is
W. McCune's OTTER. I have been using it recently in a study of
Boolean algebra. From my recent research I offer you two challenges:
one that I have met and one that I have not. In both challenges, the
function f is used to denote the Sheffer stroke, logical
nand (not of and).
In the first challenge (the one I have met), you are asked to prove that the following two equations provide a 2-basis for Boolean algebra. In other words, from the following two equations, you are asked to show that the pair provides a complete axiomatization for Boolean algebra.
f(f(f(y,f(z,x)),y),f(x,f(y,z)))=x. % Cand14 f(f(f(y,f(y,x)),y),f(x,f(y,z)))=x. % Cand16
In the second challenge, you are asked to prove that
either Cand14 or Cand16 suffices alone to
axiomatize Boolean algebra. Alternatively, you are asked to show that
Cand14 or Cand16 (each by itself) is too
weak to be a single axiom. The challenges focusing on Cand14 and
Cand16, each by itself, correspond to open questions.
An election of CADE trustees will be held soon and all AAR members will receive a ballot. The following people (listed in alphabetical order) are currently serving as trustees of CADE Inc.:
The terms of Christoph Benzmüller and Reiner Hähnle expire. Thus, there are two positions of elected trustees to fill.
The ex-officio positions of Nikolaj Bjørner and Viorica Sofronie-Stokkermans as CADE-23 program are taken by IJCAR 2012 co-chair Bernhard Gramlich.
The following candidates (listed in alphabetical order) were nominated and their statements are below:
In the CADE community I am probably best known as developer of the higher-order automated theorem prover LEO-II. LEO-II had a strong influence on the TPTP THF project, in which Geoff Sutcliffe and I, supported by further colleagues, initiated the development of a TPTP infrastructure for higher-order logic. The THF initiative led to significant improvements in higher-order automated theorem proving in the past few years.
I see CADE as the main venue for automated reasoning, and I have been very active at CADE and IJCAR conferences in the past. I am also a strong supporter of IJCAR and FLoC and the current alternation mode.
As a CADE trustee I will continue fostering the development of reasoning systems for expressive logics. Moreover, I am in favor of a further strengthening of our common infrastructure (including projects such as the TPTP, SMT-LIB, ILTP, QMLTP, etc.). This will ease the implementation, reuse, integration, and collaboration of reasoning systems, and it will reduce the effort in empirical studies. It is important that CADE continues to attract also implementation and application oriented papers while at the same maintaining its high research quality standards. I highly welcome more interaction with potential users of automated theorem provers at CADE and IJCAR.
My research focuses on theoretical, implementation and application aspects of automated reasoning. I have been working on instantiation-based methods, linear arithmetic, integration of theory reasoning, ordering constraints, orientability and AC-orderings. I have been developing and implementing iProver – an instantiation-based theorem prover for first-order logic, which won the EPR division at the recent four CASC competitions. I gave an invited talk on instantiation-based reasoning at CADE-22 and I am a conference co-chair of IJCAR 2012.
CADE has witnessed a number of success stories including: first-order and higher-order theorem proving, satisfiability modulo theories, software and hardware verification, reasoning with description and modal logics. This shows CADE excels in combining diverse research communities and fosters rapidly growing and exciting areas. I believe this tradition is vital for the success of CADE. I strongly support participation of CADE within IJCAR and FLoC which helps to achieve the goal of bringing together wider research community. Likewise, I support organisation of workshops and tutorials co-located with CADE, as these attract researchers from diverse areas and stimulate informal discussions. CADE has been excellent in supporting young researchers by providing travel grants. I believe more can be done to involve students and young researchers by e.g., organising doctoral workshops and tutorials on well-established topics of automated deduction.
CADE maintains a good balance between theoretical work, implementation and applications. I believe CADE can further strengthen interactions between the research community and real-world applications. I thoroughly support the development of new systems and competitions such as CASC, SAT and SMT-COMP which demonstrate the possibilities of state-of-the-art reasoning systems to a wide range of users and conversely, propagate problems from real-world applications to the research community.
As a CADE trustee, I would be keen in supporting and promoting high quality theoretical research, development of reasoning systems and interaction between theory and applications. I will also strongly support initiatives aiming at attracting young researchers into the area of automated deduction.
In my view, the main task of Cade Inc. is to guarantee the continuity of the CADE and IJCAR conferences, and to promote their position as the main conferences in automated deduction. The main tools of CADE Inc. are the selection of the conference chairs (with the conference sites) and the selection of the programme chairs. As for conference sites, they should be not too exotic and conferences in universities should be preferred over other venues like hotels and conference centres, because it keeps the conference cheap and flexible. I have observed that, especially for young researchers, the conference fee does play a role in their decision to attend, and young researchers are important. As for the programme chairs, they should have broad interests and care about applications.
As for CADE being the main conference in automated deduction, the main challenge is not loosing too much of the applications to other conferences while at the same time remaining sufficiently theoretically oriented. One way to do this is to stimulate different categories of papers, and to continue promoting workshops associated to CADE conferences.
Since there is ongoing controversy about how much money CADE Inc. should own, I will give my view: CADE Inc should possess enough money to compensate the losses resulting from one conference that fails due to unforeseen circumstances like volcanic ashes or political instability. But there is no need to pile up more than that.
CADE is the leading conference in automated reasoning, and the major forum for discussing all aspects of automated theorem proving, including theory, implementations and applications. I believe that progress in this field can only be achieved by supporting _all_ these aspects: new theoretical results create the basis for new powerful implementations, which in turn allow to use automated reasoning techniques in wider areas of applications. It is also essential to attract high-quality papers from new or related fields (SAT, constraint solving, computer algebra, verification, knowledge representation, complexity) as well as papers which combine automated reasoning with results from other areas. It is equally important to create the possibility of meetings – such as IJCAR – where the entire automated reasoning community meets; and to ensure the participation of IJCAR within FLoC.
Over the years I worked in several areas of automated reasoning (including non-classical logics, first-order logic and, in the last years, reasoning in extensions and combinations of logical theories). The results of my research turned out to be very useful in applications - especially in verification. I frequently publish and participate in CADE and IJCAR. I was program co-chair of CADE-23, the conference chair of FroCoS 2011, program co-chair of FTP'2009 and am regularly on the PC on numerous automated reasoning conferences. I organized several workshops (affiliated with CADE, IJCAR and ACA) with the goal of creating synergies between various scientific communities (logic, deduction, complexity; resp. deduction, symbolic computation, verification).
If elected as a CADE trustee, my goals will be:
In addition, I will fully support CADE's efforts to provide financial assistance for young researchers for attending the conference.
I believe that the advancement and application of automated reasoning depends on recognizing and supporting the synergetic interaction of theoretical progress, high performance implementation (techniques), and application requirements. I strongly support research and development that leads to effective implemented systems that are deployed in research and industrial applications. I expect CADE to remain the major forum for the presentation of new research in all aspects of automated deduction. As such CADE must reflect the depth, breadth, and interaction of all aspects of automated reasoning, to allow a broad automated reasoning community to use CADE as the preferred conference for the presentation of research results. I support CADE's efforts to provide financial assistance that enables young and poor researchers to attend the conference. I endorse CADE's leading role in IJCAR and continued participation in FLoC.
I started my academic career at Edith Cowan University in 1986, taught at James Cook University from 1992 to 2001, and am now an associate professor at the University of Miami. I am probably best known in the automated reasoning community for the TPTP Problem Library and the CADE ATP System Competitions (CASC). I have been attending CADE since CADE-10 in 1990 and have hosted CADE twice – in Australia in 1997 and in Miami in 2003. I have been on the CADE/IJCAR program committee nine times. I am responsible for publicity for CADE as an organization – I am the owner of the cadeinc.org, cadeconference.org, and ijcar.org domains, which are now the entry points to the respective web pages.
For the election of CADE trustees, as well as various internal elections, CADE and AAR have for a number of years been using a particular version of the single transferable vote (STV) algorithm, that is published as pseudo-code together with the CADE Bylaws on the CADE website.
An analysis of this algorithm has turned up two potential problems:
A revision of the algorithm was devised that solves both problems. The corrected pseudo-code has been published in place of the old version here.
I should point out that I have run the corrected algorithm on the ballots of those previous trustee elections that I had access to, and the modifications to the algorithm have not changed who was elected in any of them. One can therefore say that the flaws in the algorithm have not caused any problems until now. Still, a revision seemed in order to avoid future problems.
As a voter, one should keep in mind that ballots should list all candidates considered eligible. Listing e.g. only one candidate out of a slate of five does not mean that one does not care about the order amongst the other four, but that one does not consider them suitable for the position.
The TPTP is a well known resource for the ATP community. While there are a few concrete expenses running the TPTP, it is not easy to obtain funding for such "service" projects. The TPTP web page includes a plea for donations, and I am grateful to those people who have made contributions over the last few years. This little article is to highlight that plea. If your work benefits from use of the TPTP and related projects, consider making an annual cash donation of 100 units of a reasonable currency, to support the TPTP. A donation can be made as an unrestricted gift (tax deductable) to the University of Miami, explicitly to support the TPTP and related projects. You can read about the benefits and process of making a donation in pages linked from the TPTP web page. A premium support contract is also available. The TPTP is a community resource, so I think it deserves some community funding!
FroCoS 2011, the 8th International Symposium Frontiers of Combining Systems will take place in Saarbrücken, Germany, on 5–7 October 2011.
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 2011 wants to offer a common forum for research activities in the general area of combination, modularisation and integration of systems (with emphasis on logic-based ones), and of their practical use.
The program of FroCos 2011 will include invited talks by Alessandro Artale, Martin Lange, and Tobias Nipkow. André Platzer will give a invited tutorial on the Logical Analysis of Hybrid Systems. 15 research papers will be presented.
Regular registration is still open until 25 September.
Refer to the conference web page for details.
PLPV 2012, the 6th ACM SIGPLAN Workshop on "Programming Languages meets Program Verification" will be held in Philadelphia, USA, on 24 January, 2012. The goal of PLPV is to foster and stimulate research at the intersection of programming languages and program verification, spanning areas like types, contracts, interactive theorem proving, model checking and program analysis.
The workshop calls for submissions of up to 12 pages until 11 October, 2011.
See the workshop web page for full details.
The AI Center at SRI International is seeking a computer scientist with a strong background in ontologies, knowledge acquisition and question answering by reasoning to join a team of researchers building evaluation-driven knowledge-based systems.
Experience and Requirements: Ph.D. in Computer Science or equivalent with specialization in reasoning systems. This position requires background in ontologies and reasoning with exposure to description logics and/or logic programming, semantic web, large knowledge bases, qualitative simulation and reasoning.
See the official job posting for details.
The Research Institute for Symbolic Computation (RISC) of the Johannes Kepler University in Linz, Austria, offers a PostDoc position for the duration of 2 years starting with January 2012.
The project pursues research on a security solution whose core is a language based on classical predicate logic for specifying a property of a stream of messages transmitted over the network. The goal is to automatically translate such a specification into a program that efficiently monitors the network for a violation of the property. The core task of the PostDoc researcher is to develop the formal calculus for translating logic specifications into executable programs and to analyze the corresponding runtime/space complexity; the corresponding software development will be pursued by the partner institutions.
Applicants with a background in formal logic and automated reasoning are explicitly encouraged. Applications should be sent by 1 November 2011.
Refer to the official job posting for full details about the position and the application procedure.