[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
## [Axiom-developer] Proving Axiom Correct

**From**: |
daly |

**Subject**: |
[Axiom-developer] Proving Axiom Correct |

**Date**: |
Fri, 31 Jul 2015 18:22:27 -0500 |

I've collected all of the functions that are implemented at the
category level. For each function I've prepended the signature. These
chunks are automatically extracted during build and collected into a
file in the obj/sys/proofs subdirectory. The file has been uploaded to
http://daly.axiom-developer.org/coq.v
The file consists of a single COQ Module named Jenks.
Each category and its asssociated functions are comments in the file.
The categories in the file are arranged so that more primitive
categories occur before categories that inherit from them.
The next stage is to begin proving these algorithms correct using COQ.
Each proven function will be uncommented, along with its associated proof.
Tim