A Shell for Generic Interactive Proof Search. Alexey E. Novodvorsky, Alexey V. Smirnov
Author: Smirnov A.V., Novodvorsky A.E.
A Shell for Generic Interactive Proof Search. Alexey E. Novodvorsky, Alexey V. Smirnov
Abstract
With great amount of theorem provers, including interactive ones, it seams important to have standard tools for interactive manipulating with different logical objects as inference search tree, inference construction rule. Some interactive software like Hyperproof or MacLogic give us good examples of convinient interface, but these are not generic systems.
We have made an attempt to create a shell for generic interactive proof search, and DEDUCTIO is a result. The system supports internal representation of formulas and inference search tree, visualisation and control with different devices. It can use rules described in special metalanguge. We hope DEDUCTIO will be a step towards mixed man-machine provers.
The system is being used for teaching logic in higher school.
in English