Is it possible to use Mizar Mathematical Library for the specification of algorithms at the same detalization level as the implementation of the algorithm in industrial programming language? Mizar should be able to describe constructive proofs in maths and therefore I guess Mizar should be able to specify algorithms as well..

If algorithm is formally specified then one should be able to do automatic analysis - e.g. of running time or space requirements. Halting problem is undecidable but there should be some classes of algorithms for which one can decide/automatically prove the termination conditions. Is that possible?

If algorithms can be formally specified as one formula then one should be able to do automatic search and discovery of such algorithms - something similar like automatic theorem discovery.

Is this possible and are the ongoing work about this? Maybe deep in Mizar community?

I am aware of only one work in the field of automatic algorithm construction http://www.graco.c.u-tokyo.ac.jp/labs/morihata/paper/morihata_phd.pdf and it is more connected with the optimization and parallelization of already existing algorithms and witout use of Mizar.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.