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

Conjecture Synthesis Results

The conjecture synthesis program has been evaluated on different theories about natural numbers, lists and binary trees. Full result-files from the experiments are listed below, together with relevant Isabelle theory files.

Natural Numbers


Binary Trees

Nat Lists

These experimentes shows the decrease in search space size and run-time when it is not possble to instantiate a polymorphic list to another (possibly further nested) list.
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.