This column, as expected, offers challenges, but challenges of a different nature from those expected. Do not fear: the next column will return to a focus on theorems to prove. But for now I turn to puzzles.
Why puzzles? The answer rests with the fact that solving puzzles seems to appeal to many. Indeed, puzzle solving was the approach taken in the book Automated Reasoning: Introduction and Applications written more than thirty years ago. That book was well received, bought by many thousands, and adopted by sixty universities. And puzzles continue to fascinate people, both young and old. A quick glance at the Internet reveals numerous websites featuring puzzles ranging from crossword puzzles to logic puzzles. Here, my focus is on the latter type. I shall present two such puzzles. My objective is both to entertain you and to challenge you to use an automated reasoning program in your research.
In keeping with a discussion with a valued colleague, I also have a second objective—that of drawing new people into the field of automated reasoning. I am especially interested in those people who know so much about other aspects of computing, about at least hundreds of apps. I believe that at least a few could find most stimulating the idea of a program that reasons logically so well that it can be used to prove theorems, to design circuits, to verify computer code, and more. And the “more” brings me to a third objective.
Solving puzzles of the kind offered here may, I hope, stimulate ideas for new applications. As Martin Gardner, who wrote a monthly column in Scientific American for three decades, stated in an interview published in The Guardian, “Puzzles can lead you into almost every branch of mathematics”. My hope is that they may also lead you into branches not yet explored, or only barely explored.
I begin by offering a puzzle that some of you will view as an up-to-date version of a much older puzzle. (Be not dismayed: I shall turn shortly to a much harder puzzle, one quite difficult to solve unaided and most challenging to present to an automated reasoning program.)
Now, I confess: my original attempt at updating the puzzle led to a scenario involving three foxes and three geese. But, yes, a bright young girl pointed out that wild geese generally can fly (except for certain times of the year during breeding). So, I have reworded the puzzle and present it here, along with a challenge.
The puzzle: On one side of a deep river, three foxes and three rabbits reside. A forest fire breaks out on this side of the river. The creatures instinctively would like to cross the river to safety, and indeed a boat exists that could be used. But a serious obstacle exists: The boat is so small that it can hold only two creatures at a time. Fortunately, all the foxes and all the rabbits know how to use a boat. Unfortunately, if at any time, on either side of the river, the number of foxes outnumbers the number of rabbits, the outnumbering foxes will eat the rabbits.
The challenge: Can a sequence of moves be made so that all six creatures finally end up safely on the side of the river away from the forest fire? And, more important for our purposes here, how can an automated reasoning program be made to solve this puzzle? Pause here if you want to attempt a solution without any hints. Of course, I have assured my friends that you will not seek help from any book or online file.
If you do want a hint, I note that the puzzle can be solved with 4-and-4 and 5-and-5 instead of the conventional 3-and-3. I also note that I have on my website automatedreasoning.net a primer, in the form of one of my notebooks, that gently introduces readers to automated reasoning and the writing of clauses to express a problem or puzzle to an automated reasoning program.
And now for the harder puzzle to challenge you and your program. There are twelve billiard balls, eleven of which are identical in weight. The remaining ball—the odd one—has a different weight. You are not told whether it is heavier or lighter. You have a balance scale for weighing the balls. Can you find which ball is the odd ball in three weighings, and can you also find out whether it is lighter or heavier than the others?
Most likely, you will find the puzzle difficult to solve unaided. (Again, I trust you not to search the Internet for the answer.) And I anticipate that presenting the problem to an automated reasoning program will prove even more challenging. Indeed, when another colleague of mine, Steve Winker, showed me how to do so, I was amazed.
A sort of postscript seems in order. When I learned of this puzzle at the age of 20, I am certain that I thought the solution unique. Is that your view?
Greg Nelson, Herbrand Award laureate in 2013, passed away in early February of 2015. CADE Inc. and the entire automated reasoning community mourn his loss.
Greg Nelson was the inventor of the equality sharing method for the combination of satisfiability procedures, known as Nelson–Oppen method, after his successful collaboration with Derek Oppen on combination of theories and fast congruence closure algorithms. Greg's many pioneering and lasting contributions to theorem proving and program verification also include the development of the highly influential theorem prover Simplify, and his role in the creation of the field of extended static checking.
His name follows those of Woody Bledsoe, Harald Ganzinger, Bill McCune, and Mark Stickel in the list of Herbrand Award winners who are no longer with us, but will be always remembered.
It is with great regret that I write to share with you the news that Morgan Deters, a senior research scientist at the Courant Institute of New York University unexpectedly passed away on 17 January 2015. In September 2009, Morgan joined my research group at New York University as a research scientist to start a new project: the CVC4 SMT solver. Morgan was the lead developer and maintainer of CVC4 and led or contributed to many research projects and papers related to CVC4 and SMT.
A memorial website has been set up. There, you can share thoughts and express condolences where his family and friends will be able to see them. A link to his obituary is also posted there. Donations to the Morgan Deters Travel Award will be used to support students who wish to attend the international SMT workshop.
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-25 is
14 April 2015
Nominations pending from previous years must be resubmitted in order to be considered.
Nominations should consist of a letter (preferably as a PDF attachment) 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
Maria Paola Bonacina, President of CADE Inc.
mariapaola.bonacina (at) univr.it
with copies to
Martin Giese, Secretary of CADE Inc. and AAR
martingi (at) ifi.uio.no
Nominations are now invited for the 2015 Ackermann Award—the EACSL outstanding dissertation award for logic in computer science. PhD dissertations in topics specified by the EACSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1 January 2013 and 31 December 2014 are eligible for nomination for the award. The deadline for submission is 15 April 2015. Submission details follow below. Nominations can be submitted from 1 January 2015 and should be sent to the chair of the Jury, Anuj Dawar, by e-mail: anuj.dawar@cl.cam.ac.uk.
The 2015 Ackermann award will be presented to the recipient(s) at the annual conference of the EACSL, 7-10 September 2015, in Berlin (Germany). The award consists of
The jury is entitled to give the award to more (or less) than one dissertation in a year. The jury consists of:
The candidate or his/her supervisor should submit
The submission should be sent by e-mail as attachments to the chairman of the jury, Anuj Dawar (anuj.dawar@cl.cam.ac.uk), with the following subject line and text:
Submission can be sent via several e-mail messages. If this is the case, please indicate it in the text. Letters of support and documents can also be faxed to: Anuj Dawar, Ackermann Award, +44 1223 334678.
The Jury has the right to declare submissions to be out of scope or not to meet the requirements.
The Award is sponsored by the Kurt Gödel Society.
The Woody Bledsoe Student Travel Award was created to honor 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 Conference on Automated Deduction (CADE) or the International Joint Conference on Automated Reasoning (IJCAR), whichever is scheduled for the year, by covering part of their expenses.
CADE-25, the 25th edition of CADE, will take place 1 to 7 August 2015 in Berlin, Germany (for further information see http://cade-25.info).
The winners of the Woody Bledsoe Student Award will be partially reimbursed (e.g., between Euro 200 and Euro 750) for their conference registration, transportation, and accommodation expenses. Preference will be given to students who will play an active role in the conference (including satellite workshops, competitions, tutorials and poster events) and do not have alternative funding. However, also students in other situations are very much encouraged to apply.
A nomination consists of a recommendation letter of up to 300 words from the student's advisor. Nominations for CADE-25 should be sent by e-mail to the chairs and conference organizers at cade25@inf.fu-berlin.de.
Nominations must arrive no later than 14 June 2015. The winners will be notified by 21 June 2015.
The awards will be presented at CADE-25; in case a winner does not attend, the chairs may transfer the award to another nominee or give no award.
ITP is the premier international conference for researchers from all areas of interactive theorem proving and its applications. The sixth conference will be held this year in Nanjing.
Papers should be no more than 16 pages (LLNCS) in length. Rough diamond submissions are limited to 6 pages and may consist of an extended abstract. The deadline for abstracts is 9 March 2015. See the conference web site for details.
The Ershov Informatics Conference (the PSI Conference Series, 10th edition) is the premier international forum in Russia for research and applications in computer, software and information sciences. The conference brings together academic and industrial researchers, developers and users to discuss the most recent topics in the field. PSI provides an ideal venue for setting up research collaborations between the rapidly growing Russian informatics community and its international counterparts, as well as between established scientists and younger researchers.
There are three categories of submissions: regular papers describing fully developed work and complete results (15 pages); short papers reporting on interesting work in progress and/or preliminary results (9 pages); system and experimental papers describing implementation or evaluation of experimental systems and containing a link to a working system (7 pages). The submission deadline is 23 April 2015. See the conference web site for details.
Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. The 24th EACSL Annual Conference on Computer Science Logic will be held at the Technical University Berlin.
Authors are invited to submit papers of not more than 15 pages in LIPIcs style presenting work not previously published. The abstract submission deadline is 3 April 2015. See the conference web site for details.
TABLEAUX 2015 is the 23rd in the series of international meetings on Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2015 will be co-located with FroCoS 2015.
Tableaux methods offer a convenient and flexible set of tools for automated reasoning in classical logic, extensions of classical logic, and a large number of non-classical logics. For large groups of logics, tableaux methods can be generated automatically. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis. The conference series aims to bring together researchers interested in all aspects of tableaux—theoretical foundations, applications, and implementation techniques.
Submissions are invited in two categories: (A) Research papers, which describe original theoretical research, original algorithms, or applications, with length up to 15 pages (LLNCS); (B) system descriptions, with length up to 10 pages. Abstracts are due on 8 May 2015. See the conference web site for more information.
The 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015) will be co-located with TABLEAUX 2015. Its main goal is to disseminate and promote progress in research areas related to the development of techniques for the integration, combination, and modularization of formal systems together with their analysis.
The page limit in Springer LNCS style is 16 pages. Abstracts are due on 4 May 2015. See the conference web site for more information.
The 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2015) aims to stimulate the interaction between the two scientific communities of symbolic and numeric computing and to exhibit interesting applications of the areas both in theory and in practice. The choice of the topic is motivated by the belief of the organizers that the dialogue between the two communities is very necessary for accelerating the progress in making the computer a truly intelligent aid for mathematicians and engineers.
Proposals for workshops, tutorials, and special sessions are invited until 15 March 2015. Research papers are to be submitted until 24 May 2015, with abstracts due on 10 May 2015. See the symposium web site for more information.
The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. The 20th LPAR will be held at the University of the South Pacific, Suva, Fiji, from 24 to 28 November. Workshops will take place on 23 November.
New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices.
Regular papers of up to 15 pages (LLNCS), and short papers of up to 8 pages should be submitted until 7 July 2015. Abstracts are due on 30 June 2015. See the conference web site for details.
In addition, LPAR-20 workshops will be held either as one-day or half-day events. If you would like to propose a workshop for LPAR-20, please contact the workshop chair, Peter Baumgartner, via email (Peter.Baumgartner@nicta.com.au) by 15 May 2015.
In AAR Newsletter No. 109 (December 2014), the IJCAR Steering Committee sollicited proposals for the site of IJCAR 2016. The Committee discussed the received proposals and agreed to let IJCAR 2016 take place in Coimbra, Portuga, with Pedro Quaresma as Conference Chair.
The DL workshop is the major annual event of the description logic research community. It is the forum at which those interested in description logics, both from academia and industry, meet to discuss ideas, share information and compare experiences.
The extended paper registration deadline is 9 March 2015. See the workshop web site for details.
The 29th International Workshop on Unification (UNIF 2015) is the latest event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of identifying terms, finding solutions for equations, or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc.
UNIF is a yearly forum for researchers in unification theory and related fields to meet old and new colleagues, to present recent (even unfinished) work, and to discuss new ideas and trends. It is also a good opportunity for young researchers and scientists working in related areas to get an overview of the current state of the art in unification theory.
Submissions are abstracts (5 pages) in EasyChair style, to be submitted by 3 May 2015. See the workshop web site for details.
Determining the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, has proved to be an enabling technology for verification, synthesis, test generation, compiler optimization, scheduling, and other areas. The success of SMT techniques depends on the development of both domain-specific decision procedures for each background theory and combination methods that allow one to obtain more versatile SMT tools, usually leveraging Boolean satisfiability (SAT) solvers. These ingredients together make SMT techniques well-suited for use in larger automated reasoning and verification efforts.
The goal of the SMT Workshop is to bring together both researchers and users of SMT technology and provide them with a forum for presenting and discussing both new theoretical ideas and implementation and evaluation techniques.
Three categories of submissions are invited: extended abstracts, original papers, and presentation-only papers. The submission deadline is 30 April 2015. See the workshop web site for details.
Human reasoning or the psychology of deduction is well researched in cognitive psychology and in cognitive science. There are a lot of findings which are based on experimental data about reasoning tasks, among others models for the Wason selection task or the suppression task discussed by Byrne and others. This research is supported also by brain researchers, who aim at localizing reasoning processes within the brain. Automated deduction, on the other hand, is mainly focusing on the automated proof search in logical calculi. And indeed there is tremendous success during the last decades. Recently a coupling of the areas of cognitive science and automated reasoning is addressed in several approaches.
This workshop is intended to get an overview of existing approaches and make a step towards a cooperation between computational logic and cognitive science. Topics of interest include, but are not limited to the following: limits and differences between automated and human reasoning; psychology of deduction; common sense reasoning; logics modeling human cognition; modeling human reasoning using automated reasoning systems; non-monotonic, defeasible, and classical reasoning and possible explanations for human reasoning; and application fields of automated reasoning in the interaction with human reasoners.
The submission deadline is 1 May 2015. See the workshop web site for details.
Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressivity and lucidity of the reasoning process.
LFMTP 2015 will provide researchers a forum to present state-of-the art techniques and discuss progress.
In addition to regular papers, “work in progress” reports, in a broad sense, are also sollicited. Those do not need to report fully polished research results, but should be interesting for the community at large. Submitted papers should be in PDF, formatted using the ACM SIGPLAN style guidelines. The length is restricted to 8 pages for regular papers and 4 pages for “Work in Progress” papers. The abstract submission deadline is 30 April 2015. See the workshop web site for details.
Recently, low-level code analysis becomes of interest both from demand on system software and malware. Low-level code differs from high-level programming languages from many aspects, e.g., there are no clear distinction between code and data. Many techniques and ideas interact in low-lvel code analysis, new innovation, as well as existing ones. The workshop aims to provide a forum to discuss among researchers working in different areas and interchange/evolve ideas related to low-level code analysis.
The goal of this 1st International Workshop on Low-level Code Analysis for Security is to explore all aspects from theory to practice of low-level code analysis, including communication between industry and academia. The main outcome of this meeting will be to trigger new interactions and enrich the various approaches.
Regular papers of at most 15 pages or short papers of at most five pages are sollicited. The submission deadline is 10 May 2015. See the workshop web site for details.
Quantifiers play an important role in language extensions of many logics. The use of quantifiers often allows for a more succinct encoding as it would be possible without quantifiers. However, the introduction of quantifiers affects the complexity of the extended formalism in general. Consequently, theoretical results established for the quantifier-free formalism may not directly be transferred to the quantified case. Further, techniques successfully implemented in reasoning tools for quantifier-free formulas cannot directly be lifted to a quantified version.
The goal of the 2nd International Workshop on Quantification (QUANTIFY 2015) is to bring together researchers who investigate the impact of quantification from a theoretical as well as from a practical point of view. Quantification is a topic in different research areas such as in SAT in terms of QBF, in CSP in terms of QCSP, in SMT, etc. This workshop has the aim to provide an interdisciplinary forum where researchers of various fields may exchange their experiences.
The paper submission deadline is 8 May 2015. See the workshop web site for details.
The AMI workshop provides an informal platform for researchers interested in automated theorem proving (ATP) and interactive theorem proving (ITP), for instance, developers and users of ATP, SMT and similar systems, and developers and users of ITP systems such as Coq, HOL, Isabelle or Mizar. Its aim is the exchange of experiences and ideas for pushing these technologies further into the mainstream: to explore methods or tools from ATP that could be benefit ITP and vice versa; to advance the integration and convergence of these technologies, e.g. by considering tools and techniques from mathematics, programming languages or AI; to bring ATP and ITP work flows closer to mathematical and engineering practice.
To foster discussions, they ask for submissions of extended abstracts of 2 to 4 pages as well as for full papers of at most 15 pages. The abstract submission deadline is 7 May 2015. See the workshop web site for details.
Confluence provides a general notion of determinism and has been conceived as one of the central properties of rewriting systems. Confluence relates to many topics of rewriting and had been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constraint rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, confluence competition, and certification as well as in new applications.
The goal of the workshop is to provide a forum for researchers interested in the topic of confluence to exchange and share new developments in the field. The workshop will enable discussion on theoretical results, new problems, applications, implementations and benchmarks, and share the current state-of-the-art on the development of confluence tools.
The submission deadline is 15 May 2015. See the workshop web site for details.
The workshop aims at discussing the development and use of the first-order theorem prover Vampire. The workshop will address the newest trends in implementing first-order theorem provers, and focus on new challenges and application areas. Workshop participants will include both Vampire developers and users and provides a convenient opportunity for interesting discussions between tool developers and users. The users can learn more about Vampire and its recent developments. The developers can learn more about the use of Vampire, its efficiency in various application areas and needs of the users.
Submissions reporting on theory, application, case studies, experiments and work-in-progress using Vampire and other theorem provers in various applications are welcome. Submissions can be in any form, ranging from work in progress to completed work. Papers can be of any length, ranging from 2-page abstracts to full papers up to 20 pages in length. The submission deadline is 15 June 2015. See the workshop web site for details.
The PxTP workshop brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms. The progress in computer-aided reasoning, both automated and interactive, during the past decades, made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle larger problems progressively faster. In recent years, cooperation of such tools in larger verification environments has demonstrated the potential to reduce the amount of manual intervention. Examples include the Sledgehammer tool providing an interface between Isabelle and (untrusted) automated provers, and also collaboration of the HOL Light and Isabelle systems in the formal proof of the Kepler conjecture.
Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools to exchange problems, proofs, and models. The PxTP workshop strives to encourage such cooperation by inviting contributions on suitable integration, translation and communication methods, standards, protocols, and programming interfaces. The workshop welcomes the interested developers of automated and interactive theorem proving tools, developers of combined systems, developers and users of translation tools and interfaces, and producers of standards and protocols. The workshop is interested both in success stories and in descriptions of the current bottlenecks and proposals for improvement.
Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages) or a regular paper (up to 15 pages). The abstract submission deadline is 7 May 2015. See the workshop web site for details.
A workshop for anyone with an interest in the HOL theorem prover (HOL4) will be held at the beginning of August 2015 at CADE-25.
The theme of the workshop is the development agenda. We hope to gather both users and developers of HOL4 to brainstorm and decide: What tasks or projects (from small to large scale) should we prioritise for HOL4's continued development? How can we apply the latest developments in the fields of automated and interactive theorem proving back to HOL4, and is it worth it? Should HOL4 merge with or evolve into another system? How might we increase the amount of developer time put into the system (e.g., attracting new users, holding more workshops)?
See the workshop web site for details on how to submit an abstract.
The “Deduktionstreffen” is the annual meeting of the section “Deduction Systems” of the German Informatics Society (Gesellschaft für Informatik e.V. (GI)). It is a friendly and informal meeting with a familiar atmosphere. All members and friends of the German Deduction Community are invited to present, discuss and share their latest research results and ideas at the event.
A particular focus of the “Deduktionstreffen” is on young researchers and students, which are particularly encouraged to present their ongoing research projects to a wider audience. Another goal of the meeting is stimulate networking effects and to foster collaborative research projects.
The format of the event is as follows: Accepted abstracts are presented as 5 min teaser talks followed by a poster presentation. The (preliminary) submission deadline is 1 May 2015. See the workshop web site for details.
In this jubilee edition of CADE, we shall commemorate the multitude of proof systems that form the theoretical foundations for automated deduction. To achieve this goal, this alternative workshop proposes to bring the whole community together in a task-force to produce a concise encyclopedia of proof systems. Every entry in this encyclopedia will follow a given template and will preferably be exactly one page long, displaying the inference rules of the proof system and possibly a few clarifying remarks. The one-page encyclopedia entries will be displayed as posters during CADE.
Please visit the task-force's web site for instructions.
The SPIN workshop is a forum for practitioners and researchers interested in symbolic and state space-based techniques for the validation and analysis of software systems. Theoretical techniques and empirical evaluations based on explicit representations of state spaces, as implemented in the SPIN model checker or other tools, or techniques based on the combination of explicit representations with other representations, are the focus of this workshop.
We particularly welcome papers describing the development and application of state space exploration techniques in testing and verifying embedded software, security-critical software, enterprise and web applications, and other interesting software platforms. The workshop aims to encourage interactions and exchanges of ideas with all related areas in software engineering.
Technical research papers (at most 18 pages in LNCS format) idea papers (at most 6 pages in LNCS format), and tool presentations are sollicited. The abstract submission deadline is 17 April 2015. See the workshop web site for details.
The beautiful city of Natal is probably the best place to do Logic in Brazil. From 31 August to 4 September 2015, it will be even more so, as we are preparing for you a fascinating programme for the NAT@Logic 2015, boasting a number of striking attractions, including 10 keynote speakers, 17 tutorials, plus at least 60 contributed talks, distributed into several workshops related to Logic in Computer Science, in Philosophy, and in Mathematics.
The general preliminary submission date for contributions is 12 April 2015. Further details on abstract/paper submission are to be found in the call for papers for each event:
The aim of Automated Verification of Critical Systems (AVoCS) 2015 is to contribute to the interaction and exchange of ideas among members of the international research community on tools and techniques for the verification of critical systems.
The subject is to be interpreted broadly and inclusively. It covers all aspects of automated verification, including model checking, theorem proving, SAT/SMT constraint solving, abstract interpretation, and refinement pertaining to various types of critical systems which need to meet stringent dependability requirements (safety-critical, business-critical, performance-critical, etc.). Contributions that describe different techniques, or industrial case studies are encouraged.
The deadline for submitting regular paper abstracts is 5 June 2015. The deadline for submitting research idea papers is 7 August 2015. See the workshop web site for details.
The 10th International Satisfiability Modulo Theories Competition (SMT-COMP 2015) is part of the SMT Workshop 2015, associated with CAV 2015. The SMT Workshop and the main CAV conference will include a block of time to present the competitors and results of the competition.
1 June 2015 is the deadline for first versions of solvers. See the competition web site for details.
The 4th Confluence Competition will run live during the 4th International Workshop on Confluence (IWC 2015). Everyone developing confluence (and related) tools are invited to join CoCo 2015, to share problems and challenges.
The following categories will be run: confluence of first-order term rewrite systems (TRS); confluence of conditional term rewrite systems (CTRS); certification (CPF); and, for the first time, confluence of higher-order term rewrite systems (HRS). Tools must be registered by 19 July 2015. See the competition web site for details.
In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-25 will be held on the 4th August 2015, during the CADE-25.
Systems must be submitted by 6 July 2015. See the competition web site for details.
Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases. Research in termination analysis offers many challenges both in theory and practice. See the competition web site for details.
The Summer School Reasoning Web 2015 is primarily intended for advanced undergraduate students, M.Sc. and Ph.D. students, postdoctoral researchers, and young researchers from industry. The Summer School will also be open to a limited number of senior researchers from other areas wishing to learn about logic-based knowledge representation formalism for rules and ontologies, logic programming and reasoning and related topics in the areas.
The application deadline is 10 May 2015. See the school web site for details.
The School was designed to have something of interest to offer to each and every participant logician (or logician-to-be). This means that each participant is bound to find something of interest, and every participant is free to show interest in something. “TRS” is a recursive acronym for “TRS Reasoning School”. A bonus tutorial takes place from 24 to 28 August 2015. See the school web site for details.
It is a pleasure and an honor to take over as editor of this newsletter. I would like to thank the AAR and CADE presidents and boards for trusting me in that role. Martin Giese has been editing the newsletter since May 2008. He set the bar high for his successor in terms of reliability and diligence. His overstretched three-year term has now come to an end, but he will continue his service as Secretary of AAR (secretary@aarinc.org). As before, all requests for registration to the AAR or email address changes should be directed to him.
Most relevant calls for papers, workshops, etc., automagically end up in my mailbox, but if you want to make sure your favorite event is mentioned, please let me know directly at newsletter@aarinc.org. The newsletter is a also good place to post relevant job opportunities, new software, and open letters to the automated reasoning community.
Moreover, the newsletter is also a place where we can discuss books. As a winter solstice present from my former boss, I received a hard copy of Concrete Semantics—with Isabelle/HOL by Tobias Nipkow and Gerwin Klein (a delightful book that teaches both interactive theorem proving and semantics of imperative programming languages). This gave me the idea of introducing a Books section to this newsletter. But because book releases are not advertised widely on mailing lists, your input is sorely needed for this section. The email address is, again, newsletter@aarinc.org. Feel free (indeed, encouraged) to include brief reviews.
The world of automated reasoning is large, as I realized again when collecting the call for papers for various events. With ten workshops, seven tutorials, three system competitions, and six invited speakers, the Jubilee Edition of CADE in Berlin, Germany promises to be a major gathering. NAT@Logic in Natal, Brazil is another important event that is sure to attract many a fun-loving “Logiker”. And under the deluge of calls for papers, it is easy to miss the news that IJCAR 2016 will be held in Coimbra, Portugal.
Before that, FroCoS 2015 and TABLEAUX 2015 are co-located in Wrocław, Poland. The TABLEAUX organizers are currently evaluating the CoCon conference management system, which comes with formally verified confidentiality guarantees. CoCon reminds us that security is a growing consumer of automated deduction, whether fully automatic or interactive.
It would be impossible to close this column without mentioning a significant news item that demonstrates the growing impact of theorem proving on software engineering. It came out recently that TimSort, the default sorting algorithm for Java, is flawed. This result is the outcome of a failed proof attempt in the KeY system by Stijn de Gouw, Jurriaan Rot, Frank S. de Boer, Richard Bubel, and Reiner Hähnle. They fixed the snag and verified the new algorithm using KeY. Hats off!