User loginNavigation 
LogFun  Building Logics by Composing Functors
Logic Functors: A Toolbox of Components for Building Customized and Embeddable Logics  SÃ©bastien FerrÃ© and Olivier Ridoux :
Here's a bit more from the documentation (PDF): 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. The use of OCaml functors here may be interesting even for those who aren't into logic languages. The system allows new logics to be created in OCaml itself, by simply composing OCaml functors. This is covered further in Implementation as ML Functors. The quickest way to get a feel for what this system does is to look at the examples. (If the story subject line looks familiar to anyone, I was recently reading Guy Steele's Building Interpreters by Composing Monads...) 
Browse archivesActive forum topicsNew forum topics

Recent comments
3 hours 50 min ago
5 hours 9 min ago
5 hours 31 min ago
9 hours 2 min ago
14 hours 54 min ago
15 hours 46 sec ago
16 hours 55 min ago
1 day 2 hours ago
1 day 22 hours ago
2 days 8 hours ago