Some of you may enjoy extending the results of others. Some may enjoy experimentation designed to produce guidelines for program use. The following may, for either group, prove of interest.
The set of support strategy, relied upon by various programs, asks the user to choose from among the items defining a problem those that are to be used to initiate inference-rule application. With that strategy, typically, the initial set of support is recommended to consist of the so-called special hypothesis, the denial of the conclusion, or the join of the two. For example, if the goal is to prove in ring theory that rings in which xxx = x are commutative, the special hypothesis is the single equation xxx = x. In database problems, the situation may be far more complicated. The suggested idea is to conduct experiments that will lead to better guidance for using the set of support strategy.
For a small beginning, you might give to your program a set of targets that includes rather trivial ones. You might then have the program run a series of experiments and collect data on which elements in the chosen set of support are used some, frequently, or very often. From such experiments, you might obtain new rules for what type of item should be placed in the initial set of support.
A toy problem might provide some incentive. For an example quite unlike that focusing on ring theory, and one that is somewhat reminiscent of database inquiry, the following puzzle (from everyday language) serves nicely for illustrating an appropriate use of the set of support strategy.
Question: Who holds which jobs?
You might view the example as lacking a conclusion to be denied and lacking a special hypothesis.
Franz Baader's term as CADE trustee expired after the trustee elections 2009, and with that expired his office as president. The Board of Trustees has then elected Maria Paola Bonacina as new president of CADE.
On the behalf of CADE and AAR, I congratulate Maria Paola Bonacina on this honor and opportunity to better serve CADE and the field of automated reasoning.
Also on behalf of the AAR and CADE, I would like to thank Franz Baader for his service and commitment as president of CADE during the past six years.
Wolfgang Ahrendt
(Secretary of AAR and CADE)
The Herbrand Award is given by CADE Inc. to honor 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 IJCAR 2010 is:
April 1st, 2010
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
Maria Paola Bonacina, President of CADE Inc.
mariapaola.bonacina (at) univr.it
with copies to
ahrendt (at) chalmers.se
Some weeks after FLoC, the 3rd International Conference on Verified Software: Theories, Tools and Experiments (VSTTE) will be hosted by Heriot-Watt University in Edinburgh, August 16–19.
The goal of this conference is to advance the state of the art in the science and technology of software verification through the interaction of theory development, tool evolution, and experimental validation. Authors are encouraged to submit work in progress, particularly if the work involves collaboration, theory unification, and tool integration.
Topics of interest include specification languages, formal calculi, verification tools including theorem proving, and others which might be of interest to the AR community.
Research papers and system descriptions of up to 15 pages are to be submitted until March 29, 2010. The proceedings will be published in Springer's LNCS series.
See the conference web page for full details.
The 19th EACSL Annual Conference on Computer Science Logic (CSL 2010) will be held in Brno, Check Republic on August 23–27, 2010. 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. CSL2010 will be federated and collocated with the 35th Intl. Symp. on Mathematical Foundations of Computer Science (MFCS 2010).
Topics of interest include automated deduction and interactive theorem proving for a variety of logics, and many more which will be relevant for many in the AR community.
Papers should be submitted until March 26, 2010. Proceedings will be published in the Advanced Research in Computing and Software Science (ARCoSS) subline of Springer's LNCS series.
See the conference web page for full details.
The Second NASA Formal Methods Symposium will be held in Washington, D.C., USA, on April 13–15, 2010. NFM is a forum for theoreticians and practitioners from academia and industry, with the goals of identifying challenges and providing solutions to achieving assurance in safety-critical systems. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other safety-critical systems. The symposium aims to introduce researchers, graduate students, and partners in industry to those topics that are of interest, to survey current research, and to identify unsolved problems and directions for future research.
See the conference web page for more information.
At the time of writing, the FLoC 2010 homepage lists a stunning 52 workshops—far too many to advertise individually in an AAR newsletter1 The organizers of the following workshops have explicitly asked the editor to include an announcement:
The first workshop on Logics for System Analysis (LfSA) will be held as part of FLoC in Edinburgh, Scotland, on July 15, 2010. LfSA is affiliated with IJCAR and LICS and welcomes regular, short, and presentation-only papers on theory, applications, and tools of:
Logics for safety-critical systems; logic-based methods for development of safety-critical systems; system representations using logics, automata, modelling languages, state charts, Petri nets, dataflow models; theories, decision procedures, and calculi for system analysis; model checking, theorem proving, and systematic testing; case studies for logical system analysis; applications of system analysis to industrial problems.
In particular, contributions that bridge the gap between theory and practice or that combine different application domains are invited. Besides informal and electronic workshop proceedings, the option of a special issue in a journal after the workshop is considered.
Abstract should be submitted by March 25, 2010, full papers by April 1, 2010.
Full details are available on the LfSA website.
The second Workshop on Practical Aspects of Automated Reasoning will be held in Edinburgh, UK, on 14 July 2010. PAAR will be part of FLoC 2010 and associated with the 5th International Joint Conference on Automated Reasoning (IJCAR-2010).
PAAR provides a forum for developers of automated reasoning tools to discuss and compare different implementation techniques, and for users to discuss and communicate their applications and requirements. The workshop will bring together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools.
A short abstract of up to 10 pages should be submitted by 11 April 2010.
See the workshop website for full details.
The Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions will be held in Edinburgh, UK, on 20 July 2010. EMSQMS will be part of FLoC 2010 and associated with both IJCAR and CAV.
The EMSQMS workshop is concerned with the evaluation of logic solvers, including e.g. first-order ATP systems, SMT systems, SAT solvers, higher-order proof assistants. EMSQMS will also have a separated focus on metrics by which solvers' solutions can be evaluated. Topic of interest include:
Full papers of up to 12 pages in Easychair format and position papers about `solution quality' should be submitted by 29 March.
See The workshop website for more information.
The VERIFY workshop is concerned with all aspects of the verification of critical information systems, including in particular the application of automated deduction systems to verification tasks.
Regular papers of 6 to 15 pages reporting previously unpublished work, as well as discussion papers of 3 to 15 pages are solicited. The submission deadline is 22 March 2010.
See The workshop website for more information.
The LoCoCo 2010 workshop will be held on July 10, 2010, in Edinburg at FLoC 2010.
This workshop will focus on logic-based methods for specifying and solving complex configuration problems for software components. The goal of the workshop is to bring together both researchers and practitioners active in the area of component configuration of software systems, using different modeling and solving techniques, such as constraint and logic programing, description logics, satisfiability and its extensions. The workshop will be an opportunity to discuss common and complementary solutions for solving component configuration.
Submission deadline: Friday, March 26.
Please see the workshop website for futher instructions.
The 3rd Intl. Workshop on Invariant Generation will be held as a satellite workshop of FLoC in Edinburgh on 21 July 2010.
Generally, WING welcomes submissions presenting novel methods to support reasoning about loops in programs, including methods based on logic and automated reasoning.
Papers may be up to 15 pages in Easychair format. The deadline for submission is 8 March, 2010.
See the workshop web page for further details.
The first International Workshop on Strategies in Rewriting, Proving, and Programming will be held as part of FLoC in Edinburgh, Scotland, on July 9, 2010. This workshop is a joint follow-up of two series of workshops, held since 1997: the Strategies series held by the CADE-IJCAR community and the Workshops on Reduction Strategies (WRS) held by the RTA-RDP community.
IWS focuses on theoretical and practical research on strategies in automated deduction, interactive proving, rewriting, and programming. Contributions should be submitted by March 26, 2010. See the workshop web page for full details.
Studia Logica invites contributions to a special issue on "Logic and Natural Language", edited by Nissim Francez (Technion, Haifa) and Ian Pratt-Hartmann (University of Manchester). It is envisaged that the issue will comprise papers in two broad areas: (i) the use of logical techniques in the presentation and analysis of grammar formalisms; (ii) investigation of the logical characteristics (expressiveness, complexity, proof-theory) of natural language. They specifically, though not exclusively, invite submissions on the following topics:
Manuscripts of up to 25 pages should be subitted by: 3.9.2010.
A PDF version of the CfP with complete submission instructions may be found here.
The Technical University of Denmark (DTU, Copenhagen, Denmark) has announced a number of 3-year PhD stipends on Models and Logics for Verification and Analysis as part of MT-LAB—a VKR Centre of Excellence lead by Flemming Nielson and Kim Guldstrand Larsen and involving researchers at the Technical University of Denmark, Aalborg University and the IT University of Copenhagen.
Applications should be submitted by 1 March 2010.
Full details are available here.
The discovery of unknown lemmas, case-splits and other so called eureka steps are challenging problems for automated theorem proving and have generally been assumed to require user intervention. This thesis is mainly concerned with the automated discovery of inductive lemmas. We have explored two approaches based on failure recovery and theory formation, with the aim of improving automation of first- and higher-order inductive proofs in the IsaPlanner system.
We have implemented a lemma speculation critic which attempts to find a missing lemma using information from a failed proof-attempt. However, we found few proofs for which this critic was applicable and successful. We have also developed a program for inductive theory formation, which we call IsaCoSy.
IsaCoSy was evaluated on different inductive theories about natural numbers, lists and binary trees, and found to successfully produce many relevant theorems and lemmas. Using a background theory produced by IsaCoSy, it was possible for IsaPlanner to automatically prove more new theorems than with lemma speculation.
In addition to the lemma discovery techniques, we also implemented an automated technique for case-analysis. This allows IsaPlanner to deal with proofs involving conditionals, expressed as if- or case-statements.
A PDF of the thesis is available here.