Theorem Proving in Higher Order Logics: Emerging Trends - Proceedings

. We report on the integration of Tps as an external reasoning component into the mathematical assistant system mega. Thereby Tps can be used both as an automatic theorem prover for higher order logic as well as interactively employed from within the mega environment. Tps proofs can be directly incorporated into mega on a tactic level enabling their visualization and verbalization. Using an example we show how Tps proofs can be inserted into mega's knowledge base by expanding them to calculus level using both mega's tactic mechanism and the rst order theorem prover Otter. Furthermore we demonstrate how the facts from mega's knowledge base can be used to build a Tps library. 1 Introduction Current theorem provers, whether automatic or interactive ones, usually have strength in some specic domains while lacking reasoning power in others. Therefore there have been several attempts in recent years to combine two or more provers in order to enhance their power and facili..