System description: Interface between theorema and external automated deduction systems
|Titel||System description: Interface between theorema and external automated deduction systems|
|Buchtitel||Proc. 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS-2001)|
The interface between the Theorema system and external automated deduction systems is described. It provides a tool to access external provers within a Theorema session in the same way as “internal' Theorema provers. Currently 11 external systems are supported. The design of the interface allows combining external systems with each other as well as with “internal' Theorema provers.