MRG home page · Research · Publications · Projects · Software · People

New critics

Below is a list of ideas for new proof-planning critics that we consider implementing in IsaPlanner. More ideas for critics are welcome and will be added to the list.

CLAM 3 critics

These critics were implemented in CLAM 3

  • Generalisation of accumulator variables: When rippling-in fails to apply due to a missing sink, the generalisation critics is fired. The goal is generalised by introducing second-order meta-variables in positions of potential accumulator variables. These are then instantiated through subsequent applications of wave-rules, similarly to lemma speculation.
  • Induction scheme revision: This critic can repair proof attempts where it is necessary to use for example two-step induction instead of the standard one-step scheme. The critic is fired when no more wave-rules applies to the current goal, but a partial match, representing a missing wave-front, can be found between some wave-rule and the goal.
  • Other critics

  • Various generalisation critics using ideas from Hummel's survey of generalisation techniques for inductive proofs [hummel]. It would also be interesting to attach more types of generalisation to the lemma discovery in IsaPlanner. Currently, speculated lemmas can only be generalised through common sub-term generalisation.
  • Fertilisation critics in the presence of multiple sinks. Each sink introduced by the same variable must contain the same term. If this is not the case, the fertilisation critics would attempt to prove that the contents of the sinks are equal.
  • Fertilisation for different types of logical connectives. In Blue Book note 1238, Alessandro Armando suggests a method for implementing what is called piecewise fertilisation, which unblocks rippling when a wave-front is stuck in front of a logical connective.
  • Complementary failed proofs, as in the Dutch Flag problem (see [ireland]). This is applicable where two wave-rules can be applied, but neither will lead to fertilisation as they both leave some unproven subgoal. One meta-variable gets two different instantiations in the two failed attempts, suggesting a case-split that solves the problem.
  • References

    [hummel] Birgit Hummel, An investigation of formula generalisation heuristics for inductive proofs, Interner Bericht nr. 6/87, Universitat Karlsruhe, 1987.

    [ireland] Andrew Ireland, The use of planning critics in mechanising inductive proofs, LPAR '92: Proceedings of the International Conference on Logic Programming and Automated Reasoning, pages 178-189, 1992.

    Webpage maintained by Moa Johansson
    Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
    Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
    Please send corrections and suggestions for this page to the DReaM Support Team
    Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.