MultiAgent Theorem Proving: Towards automating the dynamics of a proof
Alan Bundy, Graham Steel · 2006
The proof planning systems available today are sequential systems. The hypothesis of this project is that the engineering of a proof planning system that is capable of dynamic, distributed, parallel proof pla nning will empower the paradigm of proof planning by unlocking its latent potential for these features. The system will be built on IsaPlanner, which is a proof planning system developed by Lucas Dixon (Dixon, 2005), based on the theorem prover, Isabelle. Alice, is an extension of Standard ML, with additional features for supporting concurrent, distributed programming. This is the choice for the implementation language for the purpose of this project. The methodology for the evaluation and the choice of test cases will also be outlined.