| ||||
| ||||
![]() Title:A Simple Semi-automated Proof Assistant for First-order Modal Logics Authors:Tomer Libal Conference:ARQNL 2018 Tags:focused sequent calculus, focused sequent calculus for first-order modal logic, higher-order logic programming, lambda prolog, proof assistant and quantified modal logic Abstract: 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 logic. The aim of this paper is to encourage the development of personal proof assistants and semi-automated provers for a variety of modal calculi. A Simple Semi-automated Proof Assistant for First-order Modal Logics ![]() A Simple Semi-automated Proof Assistant for First-order Modal Logics | ||||
Copyright © 2002 – 2025 EasyChair |