| About |
| Downloads |
| Documentation |
| FAQ |
| Contacts |
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.