HOL Provers for First-order Modal Logics - Experiments
Christoph Benzmüller – 2014
Higher-order automated theorem provers are well suited as reasoners for a wide range of quantified non-classical logics. The key idea is to exploit classical higher-order logic (HOL) as a universal meta-logic and, for example, to explicitly encode Kripke structures within this meta-logic. Experiments have shown that this approach which is orthogonal to explicit worls labeling techniques in direct theorem provers, is indeed compeititive. More recent but non-exhaustive, experiments have improved and confirmed these results. This short paper significantly further extends the experiments reported in [3]. The paper thus provides useful and relevant Information for evaluations of competitor systems. Moreover, some light is shed on the collective and individual performances of the higher order automated theorem provers LEO-II, Satallax, Isabelle, agsyHOL and Nitpick.