Motivations

Theorem provers for non-classical logics have matured dramatically in the last ten years. At one extreme, highly optimized and specific theorem provers like FACT and MSPASS can test formulae with hundreds of symbols within a few seconds. At the other extreme, generic logical frameworks like Isabelle allow us to implement almost any logical calculus as a "shallow embedding", and obtain a theorem prover for that logic by defining an associated collection of search tactics. But researchers that are merely interested in mechanising their favourite logic often find these tools too complex to modify or to program. For example, FACT is written in Lisp while Isabelle requires months to learn. In the middle are the LWB, Lotrec and LeanTap which implement many different logics or which allow users to create their own prover. The LWB provides a large (but fixed) number of logics while Lotrec requires the logic to have a binary relational semantics. If you have just invented a new tableau calculus for a logic without such semantics, then Lotrec and the LWB are not very useful. Lazy logicians, as opposed to real programmers, usually then extend LeanTap, but there is no generic LeanTap implementation that contains features like loop-checking or further optimisations. Moreover, the original LeanTap utilises various insights into the underlying Prolog engine like first argument indexing, and these are rarely understood or used in its extensions.