+ How to do Computer Algebra in Mizar

Problem description

Eventually, users will want to have things like inverse matrix for concrete 5x5 matrices quickly available in Mizar.

Solutions:

some suggestion occurred in yesterday's discussion with AdamNaumowicz:

Noaction:

current state: let the users follow the algorithms and prove that every step is correct for any computation.

Cons: very user unfriendly.

Modules wired into checker:

currently e.g. numbers are implemented this way, "+" being interpreted as the Pascal's "+" (for rational numbers).

Cons: no proof checking takes place for such computations, normal users cannot add their own algorithms, and are effectively handled as in NOACTION when a new need arises

Enhancement of MizarSchemes?

the MizarSchemes? already now are outside the standard first-order language, however, we feel save about them, because they are also proof-checked by Mizar. We could enhance them even more, to allow for a Turing-complete language inside them, proof-check them as schemes, and interpret their language in the Mizar implementation (like the MizarSchematizer? now interprets scheme inferences)

Cons: may seem too unrestricted to some purists, the implementation would cost a bit

More on this, now rather motivated by the ClusterImplementation: The cluster mechanism actually is a way how to program Mizar already now. Even though some Mizar people won't hear about it, it is actually very close to a partial Prolog implementation (functorial and conditional clusters being clauses, and their implementation a SLD derivation). The idea is to allow recursive predicate definitions (e.g. simply as Prolog programs, i.e. couple of clauses written in a cluster-like (sequent) notation), to check that e.g. given some initial conditions, these programs are finite (ending), and then use a cluster-like (more pollitically correct than Prolog-like) implementation to really do the computations in the checker. The recursively defined predicates would be handled by the system as any other predicates, the system should be able to expand the computations into a single-step proofs if the user wants it. I think there are systems (Coq?) that already implement recursive definitions, and we could have a look there for implementation ideas. -- JosefUrban - 05 Aug 2002

Automated generation of proofs

This is motivated by the work done for circuits. The proofs are generated by external programs (e.g. perl scripts) which translate the algorithms to low-level Mizar proofs based on MML theorems or schemes claiming the correctness of the basic computation steps.

Cons: length of the generated proofs (it may seem preferable to hide such proofs in the normal Mizar texts), the external proofs-generating language is not standardized in any way, nor the translation conventions and user interface (doing all of this may in practice lead to the enhancements-of-schemes solution)

-- JosefUrban - 29 Jul 2002