Logic Functors: A Toolbox of Components
for Building Customized and Embeddable Logics
Sébastien Ferré
and Olivier Ridoux
Mars 2006
Abstract: Logic Functors form a
framework for specifying new logics, and deriving automatically theorem
provers and consistency/completeness diagnoses. Atomic functors are
logics for manipulating symbols and concrete domains, while other
functors are logic transformers that may add connectives or recursive
structures, or may alter the semantics of a logic. The semantic
structure of the framework is model theoretic as opposed to the
verifunctional style often used in classical logic. This comes close to
the semantics of description logics, and we show indeed that the
logic ALC can be rebuilt using
logic functors. This offers the immediate advantage that variants of
ALC
can be explored and implemented almost for free. This report comes with
extensive appendices describing in detail a toolbox of logic functors
(definitions, algorithms, theorems, and proofs).
Keywords: logic, components,
modules and functors, theorem provers, type checking, application
developpement.
This document was translated from LATEX
by HEVEA.