Team LIS

LOGFUN
About
What is Logfun ?
This software is a library of logic functors. A logic functor is a
function that can be applied to zero, one or several logics so as to
produce a new logic as a combination of argument logics. Each argument
logic can itself be built by combination of logic functors. The
signature of a logic is made of a parser and a printer of formulas,
logical operations such as a theorem prover for entailment between
formulas, and more specific operations required by Logical Information
Systems (LIS). Logic functors can be concrete domains like integers,
strings, or algebraic combinators like product or sum of logics.
It is developped by Sébastien
Ferré in project
LIS at IRISA.
How does it work ?
Logic functors are coded as Objective Caml modules. A logic semantics
is associated to each of these logic functors. This enables to define
properties of logics like the consistency and completeness of the
entailment prover, and to prove under which conditions a generated
entailement prover satisfies these properties given the properties of
argument logics.
License
This software is ditributed under the GNU General Public
License.
It is registered at the APP with
IDDN FR 001 290003 000 S P 2005 000 10800.
Related publications
You can find here some publications
at the origin of this software.
