On Sun, 2 Nov 2014, Bohua Zhan wrote:
Two examples are given at the end: the first refers to the permutation
example in section 6.4 of the new Isabelle Cookbook manual, rewriting:
Note that the Isabelle Cookbok is not really "new". It is useful to get
started in some areas of Isabelle/ML usa
Hi, Tobias
Thanks for the reply. My main motivation here is to try to write
something that more closely resembles how humans think. I understand
this is very far from being able to be included in the main
repository. This is just to explore different approaches.
In particular I would be intereste
Hi Bohua,
There is an awful lot of literature on rewriting which you may want to look at.
A good starting point is the practically unbeatable equational prover
Waldmeister http://www.waldmeister.org/ which is also available via
sledgehammer. It uses something called unfailing completion, which
Hi, everyone
My name is Bohua Zhan, a postdoc in mathematics at MIT. I am
interested in doing some experiments in automated proof techniques in
Isabelle. I have been reading the documentations and existing code for
some time, but this is my first attempt at writing some code, so here
it is (attach
