Description: |
GLEFatinf: a graphic framework for combining theorem provers and editing proofs for different logics. A running system for combining theorem provers, editing and checking proofs in different logics is presented. It is based on a formalism similar to and developed from the Calculus of Constructions (Coquand and Huet). Its abilities are independent of the logic and the calculus used. It is therefore possible to present and combine proofs coming from any theorem prover. The user may define the full graphic presentation of proofs, formulas,... he wishes. Some other original features are: proofs can be viewed and browsed in different ways, (parts of) proofs can be memorized and reused, the size of inference steps for proof presentation can be fixed arbitrarily, symmetries can be handled in a natural manner, equational and non equational proofs are treated in an homogeneous way,... The principles of the underlying formalism and the several languages used are given. The system has been implemented on Macintosh (and will soon be transported on SUN workstations). The system should also allow an easy integration of theorem provers with symbolic computation systems. Several running examples in classical and non-classical logics show evidence of the capabilities of the system. In particular, we present an OTTER [McC90] proof in which we handle symmetries in the proved theorem. Finally, the main lines of current and future work are given. |