This tutorial aims at introducing the Tableaux/FroCoS community to the Concurrent Logical Framework (CLF) and the Celf tool, as well as some of their applications.
A logical framework is a meta-language to specify and reason about deductive systems, as found in logic or programming language theory. The resulting specifications are executable and help reason about languages in a clear and simple way.
CLF is a logical framework for specifying and implementing concurrent systems. It is an extension of the LF framework with (i) linear types to support representation of stateful computation and (ii) a monad to support representation of concurrency. As a result, term equality in this language is not only defined modulo α-renaming but also modulo let-floating, which allows CLF signatures to be interpreted as concurrent logic programs.
Celf is an implementation of CLF, as Twelf is for LF. It allows the user to specify a concurrent system and provides them with type checking, type reconstruction and proof search. However, it does not yet include the meta-theoretic capabilities that Twelf has; this is under current investigation.
We will illustrate the CLF approach and the usage of Celf in a step-by-step manner by going
from a simple encoding of producer/consumer Petri nets to the more involved example of
the concurrent λ-calculus, showing how the various features of the framework combine
to allow clear formalisation of these concurrent systems.
This tutorial gives an introduction on how to implement an automated theorem prover. Starting with the sequent calculus, we show how to translate the axiom and the rules of the calculus step by step into a Prolog program that can be used to automate proof search in the sequent calculus.
After dealing with propositional logic, we extend this program step by step in order to obtain a complete and sound theorem prover for classical first-order logic. Afterwards, we show how these concepts can be used to implement more efficient theorem provers based on tableau and connection calculi.
The tutorial contains many examples to illustrate all of the presented techniques. These techniques are general enough to implement any (formal) proof calculus and can easily be adapted, e.g., to implement a theorem prover based on a calculus for non-classical logics. A short introduction into Prolog is given in the first part of this tutorial.