mmj2 Proof Assistant
(back to Start.html)
The Start.html
diagram shows "mmj2 Proof Asst" at the center, but the object in the
center of the diagram actually consists of more than just the main
(server) Proof Assistant program.
Before the Proof Assistant is triggered, the input RunParms.txt file is processed and actions are taken accordingly. Then, if there are no serious errors and the input Metamath .mm database file has been successfully parsed, the main Proof Assistant program is called.
From the user's perspective, the main Proof Assistant program is "management". It receives requests, primarily from the Proof Assistant GUI screen, calls other programs as needed to satisfy the requests, and send the results back, along with any error messages.
(back to Start.html)