Christoph Benzmuller
Saarland University (on leave)

"Automating Access Control Logics and Multimodal Logics in the Automatic Higher-Order Theorem Prover LEO-II"


LEO-II is a standalone, resolution-based higher-order theorem prover designed for effective cooperation with specialist provers for natural fragments of higher-order logic. At present LEO-II can cooperate with the first-order automated theorem provers E, SPASS, and Vampire. LEO-II is implemented in Objective Caml and its problem representation language is the new TPTP THF language. We demonstrate that problems in normal multimodal logic and access control logics can be elegantly encoded simple type theory and automated in LEO-II.


Back to Talks Page