On the Computational Interpretation of CKn for Contextual Information Processing – Ancillary Material
|Professorship/Faculty:||Foundations of Computer Science||Authors:||Scheele, Stephan M. ; Mendler, Michael|
|Publisher Information:||Bamberg : opus||Year of publication:||2014||Pages / Size:||38 S.||Series ; Volume:||Bamberger Beiträge zur Wirtschaftsinformatik und Angewandten Informatik ; 91||Year of first publication:||2013||Language(s):||English||Licence:||German Act on Copyright||URN:||urn:nbn:de:bvb:473-opus4-101139||Document Type:||Other||Abstract:||
In the journal article we introduce a modal λ-calculus λCKn whose type system corresponds to the constructive multi-modal logic CKn. This logic is a constructive refinement of the classical multi-modal logic CKn which forms the heart of the class of description logics used in semantic information processing. λCKn constitutes the core of a functional language for information processing in this application domain. Being strongly typed, it offers static type checking to support safe contextual reasoning in relational structures like those treated by description logics.
Here we provide detailed mathematical proofs for the results presented in . Accordingly, this report is not meant as a self-contained technical exposition of the whys and hows of λCKn. It is merely a collection of ancillary material to complement the main article  to which the reader is referred for more information.
An early version of this work appeared at the 3rd International Workshop on Logics, Agents and Mobility (LAM 2010). We are grateful for the support by the German Research Council (DFG) who funded this research as part of the project SPACMODL under grant No. ME 1427/4-1.
|SWD Keywords:||Modallogik ; Informationsverarbeitung||DDC Classification:||004 Computer science
|URI:||https://fis.uni-bamberg.de/handle/uniba/6157||Release Date:||21. May 2014|