Logic Functors: A Toolbox of Components for Building Customized and Embeddable Logics

Sébastien Ferré 1 Olivier Ridoux 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
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 $\calALC$ can be rebuilt using logic functors. This offers the immediate advantage that variants of $\calALC$ 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).
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00070155
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 7:16:38 PM
Last modification on : Friday, November 16, 2018 - 1:22:21 AM
Long-term archiving on : Sunday, April 4, 2010 - 8:20:11 PM

Identifiers

  • HAL Id : inria-00070155, version 1

Citation

Sébastien Ferré, Olivier Ridoux. Logic Functors: A Toolbox of Components for Building Customized and Embeddable Logics. [Research Report] RR-5871, INRIA. 2006, pp.103. ⟨inria-00070155⟩

Share

Metrics

Record views

184

Files downloads

180