To set the stage for this column, I begin with a few lines from the February 2012 column.
Proof length, the length of a given proof, is of interest to various mathematicians and logicians today, and has been in the past. By length, I do not include the axioms used in a proof; rather, I count merely the deduced equations or deduced formulas. For example, the logician C. A. Meredith was indeed interested in finding so-called short proofs. Logicians who followed him took up the activity.
Meredith was also interested in single axioms, the shorter the better.
For classical propositional calculus, he found a 21-letter single axiom,
the following, in which the function i denotes implication and the
function n denotes negation.
P(i(i(i(i(i(x,y),i(n(z),n(u))),z),v),i(i(v,x),i(u,x)))).
His proof has length 41 (applications of condensed detachment), which is captured (with hyperresolution) in the following clause.
-P(i(x,y)) | -P(x) | P(y).
Your challenge is first to find a proof, preferably of length 41, that deduces from the Meredith single axiom the Lukasiewicz 3-axiom system, the following in 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))).
Then, far more challenging (especially if you do not consult the literature), you are asked to find a shorter proof that deduces the Lukasiewicz 3-axiom system.
Yes, such does exist.
This last challenge is indeed formidable.
The CADE Board of Trustees has recently established a Best Paper Award to be given at each future CADE conference. In short terms:
At every CADE conference the Program Committee selects one of the accepted papers to receive the CADE Best Paper Award. The award recognizes a paper that the Program Committee collegially evaluates as the best in terms of originality and significance, having substantial confidence in its correctness. Under exceptional circumstances, the Program Committee may give two awards (ex aequo) or give no award. The CADE Best Paper Award is permanently established beginning with CADE-24 in 2013.
For a slightly extended description of the Award, please refer to the CADE Inc. web site.
The 7th International Joint Conference on Automated Reasoning (IJCAR) will take place in Vienna, Austria on 19–22 July 2014.
IJCAR is the premier international joint conference on all topics in automated reasoning. The IJCAR technical program will consist of presentations of high-quality original research papers, system descriptions, and invited talks. IJCAR 2014 is a merger of leading events in automated reasoning:
IJCAR 2014 invites submissions related to all aspects of automated reasoning, including foundations, implementations, and applications. Original research papers and descriptions of working automated deduction systems are solicited. The proceedings of IJCAR 2014 will be published by Springer-Verlag in the LNAI/LNCS series.
Important dates:
Travel awards will be available to enable selected students to attend the conference. Details will be published in March 2014.
Full details are available on the IJCAR website.
The Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications will take place in Vienna, Austria, on 14–17 July 2014.
This joint RTA and TLCA conference is the major forum for the presentation of research on all aspects of rewriting and typed lambda-calculi. Topics of interest include theorem proving and proof assistants for the logics in question.
Research papers of at most 15 pages in Springer format are to be submitted by 4 February 2014, with abstracts due 28 January.
For more details, including submission instructions, see the conference web site.
ECAI'14, the Twenty-first European Conference on Artificial Intelligence will be held in Prague, Czech Republic, on 18-22 August 2014.
The biennial European Conference on Artificial Intelligence (ECAI) is Europe's premier archival venue for presenting scientific results in AI. Organised by the European Coordinating Committee for AI (ECCAI), the ECAI conference provides an opportunity for researchers to present and hear about the very best research in contemporary AI. As well as a full programme of technical papers, ECAI'14 will include the Prestigious Applications of Intelligent Systems conference (PAIS), the Starting AI Researcher Symposium (STAIRS), the International Web Rule Symposium (RuleML) and an extensive programme of workshops, tutorials, and invited speakers. (Separate calls are issued for PAIS, STAIRS, tutorials, and workshops.)
High-quality original submissions are welcome from all areas of AI, including Reasoning and Logic. The deadline for paper submission is 1 March 2014.
For full details, go to the ECAI web site.
WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. The 21st WoLLIC will be held in Valparaiso, Chile, on 1–4 September 2014.
Papers in Springer LNCS format are to be submitted until 28 March 2014, abstracts due on 24 March. Please refer to the workshop web page for details.
The 8th International Conference on Tests and Proofs, TAP 2014, will take place in York, UK, on 24–25 July 2014.
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 March 2014, abstracts are due on 25 February. TAP also invites tutorial proposals.
For detailed information, see the conference web site.
The 26th International Conference on Computer Aided Verification, CAV'14, will be held in Vienna, Austria, on 18–22 July 2014. 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.
Abstract submission closes on 31 January 2014, full papers are to be submitted by 7 February 2014.
Refer to the CAV website for registration instructions.
In AAR Newsletter #103 (July 2013), the CADE Board solicited proposals for the site of CADE-25, to be held in 2015. The Board discussed the received proposals, and agreed to let CADE-25 take place in Berlin, Germany, with Christoph Benzmüller as Conference Chair.
The 10th International Workshop on Automated Deduction in Geometry, ADG 2014, will be held at the University of Coimbra, Portugal,on 9–11 July 2014. ADG will be co-located with CICM 2014, Conferences on Intelligent Computer Mathematics, 7-11 July.
ADG is a forum to exchange ideas and views, to present research results and progress, and to demonstrate software tools on the intersection between geometry and automated deduction.
The submission deadline is 4 May 2014. See the Workshop web page for full details.
Peter Baumgartner and Richard Waldinger are asking for contributions to a book of collected articles presenting research in all aspects of automated reasoning, in particular the design of automated reasoning systems and their applications.
A common theme behind Mark Stickel's work was developing techniques for building better automated reasoning systems. His discoveries were ground-breaking and include AC-unification, reasoning modulo a theory, term indexing, and thorough development of the SNARK and PTTP provers. In 2002 he received the Herbrand award for all his work, the highest award in automated reasoning.
The editors would like to honour Mark's achievements by editing a Festschrift comprised of articles in the spirit of his research approach: developing fundamental techniques driven by practical applications and informed by rigorous theory.
High-quality submissions are invited on the general topic of automated reasoning and its applications, especially but not exclusively to the design of automated theorem proving systems, with connections to any of Mark Stickel's research areas:
The deadline for submissions is 1 March 2014, but authors are asked to notify the editors as early as possible of their intent to submit a paper.
See the project web page for further details, including submission instructions.