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.

Titel
HOL Provers for First-order Modal Logics - Experiments
Verfasser
Christoph Benzmüller
Datum
2014-07
Erschienen in
EasyChair, EPiC Series
Größe oder Länge
pp. 1-106