Last Release: 2009
A proof planner for Isabelle which implements dynamic rippling for the various logics in Isabelle. Lemma discovary for IsaPlanner have recently being developed.
Last Release: 2003
A proof planner implemented in Lambda-Prolog with a implementation of dynamic rippling and some proof critics.
Last Release: 1999
A linking between the HOL interactive theorem prover and the Clam system. It provides a way to execute the proof plans found by Clam in HOL. Written in SML and Prolog.
Last Release: 1998
An implementation of rippling for the NuPRL system.
Last Release: 1997
A first order inductive theorem prover implementing coloured rippling in Alegro Common Lisp.
Last Release: 1996
A first-order proof planner, implemented in Prolog, with a version of static rippling and Ireland`s proof critics.