A Simple Semi-automated Proof Assistant for First-order Modal Logics

The 3rd International Workshop for Automated Reasoning in Quantified Non-Classical Logics (ARQNL)
Oxford, England


Most theorem provers and proof assistants are written in imperative or functional programming languages. Recently, the claim that higher-order logic programming languages might be better suited for this task was revisited and a new interpreter, as well as new proof assistants based on it, were introduced. In this paper we follow these claims and describe a concise implementation of a prototype for a semi-automated proof assistant for first-order modal logics. The aim of this paper is to encourage the development of personal proof assistants and semi-automated provers for a variety of modal logics.