Higher Order Logic reasoning experiments, extracted from Programming and Proving in Isabelle/HOL by Tobias Nipkow.
It contains the following experiments:
-
NatSimpleTest.metta: prove really simple assertions such as 2 + 2 = 4. -
NatTest.metta: prove more complex properties such x + Z = x. However, there is a little bit of cheating involved such as adding the inductive property in the axioms. -
NatStandaloneTest.metta: prove that x + Z = x without cheating. For that it uses its own chainer instead of relying on the synthesizer. -
ListTest.metta: prove theorems on lists such that list reversion is involutive.