logics

This page should outline the varieties existing between the logical foundations of existing proving tools, and at the same time underline the important common ground between all these logics.

It may be necessary to stress the distinction between higher-order logic and first-order logic, although tools that are supposedly first order often provide extensions that give them an expressive power that is comparable to higher-order logic.

For the common ground between all the proof systems, a clear description of the common ways to represent both data-structures and computing structures should be outlined. In the same spirit as Wiedijk's "seventeen theorem provers" document, explanations of encoding for basic data-structures could be provided. An overview of problems that have already been handled in several theorem provers could be constructed just now.