SPACMoDL

Research Project

Semantic Processing and Auditing in Constructive Modal Description Logic

(SPACMoDL)

Funded by the German Research Council (DFG) under ME 1427/4-1.

Duration

2008 - 2011

Topic

The research project aims at investigating innovative, semantic driven audit models that are based on formal models of data and audit process logic which will be represented through ontologies and their conversion in a synchronous, dataflow-based execution model.

New constructive modal logics will be developed for this purpose which can be used in a descriptive manner as static typesystems on the one hand and for automated generation of executeable audit processes on the other hand.

The logic is based on description logics which are in widespread use in applications of the semantic web but is extended to cover a constructive notion of truth to capture the gametheoretic-aspect and the uncertainty aspect of auditing procedures.

Since auditors need reliable tools to draw the right consequences the application has strong requirements on the correctness of software (certified code) so that mathematically strong methods are needed. Our target is the creation of an advanced software architecture for financial auditing which does justice to the rising requirements for flexibility, scalability, user friendliness and efficiency in this domain.

Publications

M. Mendler, S. Scheele: Constructive Description Logic cALC as a Type System for Semantic Streams in the Domain of Auditing. Logics for Agents and Mobility (LAM'08), Hamburg, August 2008.

M. Mendler, S. Scheele: Towards Constructive Description Logics for Abstraction and Refinement.Int'l Workshop on Description Logic (DL 2008), Dresden, May 2008.

Mendler, M. & Scheele, S. (2009), Towards a Type System for Semantic Streams. Stream Reasoning 2009, in 'Stream Reasoning 2009, Heraklion, Crete'.

Mendler, M. & Scheele, S. (2009), 'Towards Constructive DL for Abstraction and Refinement', Journal of Automated Reasoning.

Mendler, M. & Scheele, S. (2009), Exponential Speedup in UL Subsumption Checking relative to general TBoxes for the Constructive Semantics, 22nd International Workshop on Description Logics (DL 2009), Oxford, UK, July 27-30, 2009

Mendler, M. & Scheele, S. (2010), 'Towards a Simply Typed CALculus for Semantic Knowledge Bases', 3rd Workshop on Logics for Agents and Mobility (LAM)

Mendler, M. & Scheele, S. (to appear), 'Cut-free Gentzen Calculus for Multimodal CK', Journal of Information and Computation

Talks

Scheele, S. (2006), Semantisch orientierte Verarbeitung von Massendaten in der Betriebs- und Wirtschaftsprüfung, VDI/VDE München, June 2006

Scheele, S. (2008), Towards Constructive Description Logic for Abstraction and Refinement. Theory Seminar, University of Birmingham, April 2008

Scheele, S. (2008) cALC: Towards Constructive DL for Abstraction and Refinement. 24th British Colloquium for Theoretical Computer Science (BCTCS 2008), Durham, April 2008

Scheele, S. (2008) Towards Constructive Description Logics for Abstraction and Refinement.Int'l Workshop on Description Logic (DL 2008), Dresden, May 2008.

Scheele, S. (2008) Semantic Stream Processing in Business Auditing. International Open Workshop on Synchronous Programming (Synchron 2008) Aussois, December 2008

Scheele, S. (2009) Towards a Type System for Semantic Streams. Stream Reasoning 2009, Heraklion, Crete, May 31, 2009

Mendler, M. (2009) Exponential Speedup in UL Subsumption Checking relative to general TBoxes for the Constructive Semantics, 22nd International Workshop on Description Logics (DL 2009), Oxford, UK, July 27-30, 2009

Scheele, S. (2010) Project SPACMoDL, State of Affairs & Forecast for Future Work. Monday Afternoon Club (MAC), University of Bamberg, January 2010

Mendler, M. (2010) Towards a Simply Typed CALculus for Semantic Knowledge Bases, 3rd Workshop on Logics for Agents and Mobility (LAM), associated with LICS 2010, July 15, 2010

Scheele, S. (2010) Towards a Simply Typed CALculus for Contextual Information Flow, 17th International Workshop on Types for Proof and Programs, Warsaw, Poland, October 13- 16, 2010

Mendler, M. (2011) On the Curry-Howard Correspondence for Constructive Modal Logic CK , 18th International Workshop on Types for Proof and Programs (associated with CSL 2011), Bergen, Norway, September 8--11 2011