Section: Research Program

Libraries

Rather than importing proofs from one system, transforming them, and exporting them to another system, we can use the same tools to develop system-independant proof librairies. In such a library, each proof is labeled with the logics in which it can be expressed and so with the systems in which it can be used.