I plan, when I have all in hand, to tell you some pleasing stories – stories that show that automated reasoning is indeed most relevant to various mathematicians. I also plan, if things go as I intend, to offer more problems from areas of algebra. For now, however, I offer another problem from logic as a challenge.
For this challenge, the credit goes to H. Hiz and his presentation in 1959. In place of condensed detachment, Hiz offered three inference rules to use, the following, which are captured with three clauses and the use of hyperresolution.
-P(i(x,y)) | -P(i(y,z)) | P(i(x,z)). -P(i(x,i(y,z))) | -P(i(x,y)) | P(i(x,z)). -P(i(n(x),y)) | -P(i(n(x),n(y))) | P(x).
The function n denotes negation, and the function
i
denotes implication. Hiz offered the following 2-basis.
P(i(n(i(x,y)),x)). P(i(n(i(x,y)),n(y))).
At the most general level, one problem asks you to show, as Hiz did, that the use of the three given inference rules suffices to show that the cited 2-basis provides an axiomatization for classical propositional calculus.
The problem here is, instead, to produce what was missing for more than four decades, namely, a first-order proof that the given 2-basis offers what is needed. (The problem was brought to my attention in 2004 by my colleague Branden Fitelson.) In other words, a proof existed, but not the type of proof featured in much of automated reasoning, in particular, a first-order proof.
I suggest as a target the well-known 3-basis of Lukasiewicz, the following, given in its negated form.
-P(i(i(p,q),i(i(q,r),i(p,r)))) | -P(i(i(n(p),p),p)) | -P(i(p,i(n(p),q))) $ANS(step_allLuka_1_2_3).
Of course, you may choose for your target some other well-known basis for this area of logic.
For those of you who wish a further challenge, I suggest that you find a 10-step proof. Yes, I do have such. Warning: the sought-after 10-step proof may require a substantial amount of computer time, regardless of the program you use. Indeed, in 2004 I waited a very, very long time before the desired proof was returned to me by W. McCune's program OTTER. Further, can you find a proof of length strictly less than 10?
in recognition of his outstanding contributions to tableau-based theorem proving in classical and non-classical logics, as well as to many other areas of Automated Reasoning, Logic Programming, and Philosophical Logic.
The Award will be presented at IJCAR 2012, The 6th International Joint Conference on Automated Reasoning, June 26, 2012.
IJCAR 2012 is a merger of leading events in automated reasoning:
IJCAR 2012 will be held at the University of Manchester, UK, from 26 June to 1 July, 2012.
Early registration will end on 25 May, and late registration on 11 June. To register, please go to the registration page.
The Woody Bledsoe Student Travel Award was created to honour 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 Joint Conference on Automated Reasoning (IJCAR) or the International Conference on Automated Deduction (CADE), whichever is scheduled for the year, by partially covering of their expenses. The winners of the travel award will be (partially) reimbursed for their conference registration, transportation, and accommodation expenses (past awards have varied, but have typically been £120 to £500). 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.
The application deadline is 14 May. Applicants will be notified by 21 May.
See here for details about applications.
The 2nd International Workshop on Computer Theorem Proving Components for Educational Software will take place at Jacobs University, Bremen, Germany, on 11 July 2012, in association with CICM 2012.
This workshop intends to gather the research communities for Computer Theorem proving (CTP), Automated Theorem Proving (ATP), Interactive Theorem Proving (ITP), as well as Computer Algebra Systems (CAS) and Dynamic Geometry Systems (DGS). The goal of this union is to combine and focus systems of these areas to enhance existing educational software as well as studying the design of the next generation of mechanised mathematics assistants (MMA).
Extended abstracts of 5–8 pages are solicited until 15 May. See the workshop web page for details.
The 4th Intl. Workshop on Invariant Generation will be held as a satellite workshop of IJCAR in Manchester, UK, on 30 June 2012.
Generally, WING welcomes submissions presenting novel methods to support reasoning about loops in programs, including methods based on logic and automated reasoning.
WING still welcomes submissions of one-page abstracts of work in progress, new ideas, tools under development, as well as work by PhD students, until 15 May.
See the workshop web page for further details.
LoCoCo2012, the Third International Workshop on Logics for Component Configuration will take place in Budapest, Hungary, on 8 September 2012, co-located with ICLP'12.
The workshop will focus on logic-based methods for specifying and solving complex configuration problems. The goal of the workshop is to bring together both researchers and practitioners active in the area of component configuration of systems, using different modeling and solving techniques, such as constraint and logic programming, description logics, satisfiability and its extensions. The workshop will be an opportunity to discuss common and complementary solutions for solving component configuration.
Research papers and system descriptions should be submitted until 20 June 2012.
For more details, please refer to the workshop web site.
The Department of Computer Science of the Università degli Studi di Verona, in beautiful Verona, Italy, has one opening for a post-doc position in
The position is for one year (12 months), possibly renewable. It is funded by the University and therefore is not attached to a research grant or project with a pre-defined topic: the successful applicant is welcome to contribute research themes. The position is full-time on research (no teaching assignments) so that there is time and freedom to pursue more than one direction. Recent Ph.D. graduates or Ph.D. students very close to graduation in Computer Science or related field with a thesis in automated reasoning (broadly meant) are kindly invited to write by e-mail, attaching their Curriculum Vitae with a research statement, to:
Prof. Maria Paola Bonacinafor further details and discussion of research interests. The position should be filled by September 2012. Applications will be considered as soon as received.
Artificial Intelligence Journal (AIJ) is one of the longest established and most respected journals in AI, and since it was founded in 1970, it has published many of the key papers in the field. The operation of the Editorial Board is supported financially through an arrangement with AIJ's publisher, Elsevier. The editorial board of Artificial Intelligence is now in the unique position of being able to make available substantial funds, of the order of US$250,000 per annum to support the promotion and dissemination of AI research.
The deadline for proposals for the next round of fundings is 13 May 2012. See the AIJ editorial web site for details.