Re: [Axiom-developer] Proving Axiom Correct

[Raymond Rogers]

Great!  Actually this list makes a great dictionary for me :)

Might I suggest opening an axiom-developer forum where discussions about 
different categories,  proofs, and typos can be addressed 
individually?   And perhaps a prefered format for the signatures along 
the ideas of input-process-output as blocks together with a "lint" and 
cross reference program.
Even with the correct semantic,s syntax/form can still make things 
unmaintainable; I know I have done it.  Written perfectly correct 
code/mathematical solutions that totally mystified me later.

Ray

On 07/31/2015 07:22 PM, address@hidden wrote:
> 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
>
> _______________________________________________
> Axiom-developer mailing list
> address@hidden
> https://lists.nongnu.org/mailman/listinfo/axiom-developer