Poitín: distilling theorems from conjectures We describe a new fully automatic theorem prover called Poitín which makes use of a novel transformation algorithm called distillation to prove input conjectures. The input conjectures are defined in a functional language and are transformed using the distillation algorithm. The result of this transformation can be easily inspected to see whether the original conjecture is true. Possible divergence of the transformation algorithm is detected, and this information is used to perform generalizations to ensure termination. We give several examples of the application of the theorem prover, and compare it to related work.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Hamilton, G.W.: Poitín: distilling theorems from conjectures (2006)