Logic Functors : a Framework for Developing Embeddable Customized 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-based applications often use customized logics which are composed of several logics. These customized logics are also often embedded as a black-box in an application. So, implementing them requires the specification of a well-defined interface with common operations such as a parser, a printer, and a theorem prover. In order to be able to compose these logic, one must also define composition laws, and prove their properties. We present the principles of logic functors and their compositions for constructing logics that are ad-hoc, but sound. An important issue is how the operations of different sublogics inter-operate. We propose a formalization of the logic functors, their semantics, implementations, proof-theoretic properties, and their composition.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00072131
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 7:52:01 PM
Last modification on : Friday, November 16, 2018 - 1:22:21 AM
Long-term archiving on : Sunday, April 4, 2010 - 10:54:42 PM

Identifiers

  • HAL Id : inria-00072131, version 1

Citation

Sébastien Ferré, Olivier Ridoux. Logic Functors : a Framework for Developing Embeddable Customized Logics. [Research Report] RR-4457, INRIA. 2002. ⟨inria-00072131⟩

Share

Metrics

Record views

146

Files downloads

185