SPACMoDL

Semantic Processing and Auditing in Constructive Modal Description Logic (SPACMoDL)

2008 - 2014

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

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

New constructive modal logics are developed for this purpose which can be used in a descriptive manner as static type systems 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 are extended to cover a constructive notion of truth to capture the game-theoretic 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.

Mendler, M. & Scheele, S. (2008) 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. 

Mendler, M. & Scheele, S. (2008) Towards Constructive Description Logics for Abstraction and Refinement. International Workshop on Description Logics (DL 2008), Dresden, May 2008.    

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

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

Aguado, J. & Macias, F. & Mendler, M. (2009), The Lusterel Library: Programming Combined Data and Control Flow Applications in Haskell. ACM SIGPLAN 2009 Developer Tracks on Functional Programming (DEFUN 2009) in conjunction with The 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009). Edinburgh, Scotland, September 2009.

Mendler, M. & Scheele, S. (2010), Towards Constructive DL for Abstraction and Refinement, Journal of Automated Reasoning, Vol. 44, No. 3.

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

Mendler, M. & Scheele, S. (2011), Cut-free Gentzen Calculus for Multimodal CK, Journal of Information and Computation 209, 12 (December 2011), 1465-1490.

Aguado, J. & Mendler, M. (2011) Computing with Streams. Declarative Aspects of Multicore Programming (DAMP 2011), ACM Proceedings, ISBN 978-1-4503-0486-3, pp. 35-44, Austin, Texas, USA, January 2011.

Aguado, J. & Mendler, M. (2010) Towards Strategies for Dataflow Programming. Implementation and Application of Functional Languages. (IFL 2010). Utrecht University, Netherlands, September 2010.

Mendler, M. & Scheele, S. (2013), On the Computational Interpretation of CKn for Contextual Information Processing - Ancillary Material, Technical Report 91/2013, Faculty of Information Systems and Applied Computer Sciences, The Otto-Friedrich-University of Bamberg, Germany

Mendler, M. & Scheele, S. (2014), On the Computational Interpretation of CKn for Contextual Information Processing, Fundamenta Informaticae, Vol. 130.

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) SPACMoDL - Semantic Processing and Auditing in Constructive Modal Description Logic - State of Affairs - FSAE1. Datev eG, Nürnberg, January 2009.

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. (2009) SPACMoDL - Semantic Processing and Auditing in Constructive Modal Description Logic - State of Affairs & Introduction to RDF and Typed Streams. dab:GmbH, Deggendorf, December 2009

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

Scheele, S. & Kuhndörfer, T. (2010) SPACMoDL - Semantic Processing and Auditing in Constructive Modal Description Logic - State of Affairs - VISFSAE. Datev eG, Nürnberg, 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.

Scheele, S. (2011) SPACMoDL - Semantic Processing and Auditing in Constructive Modal Description Logic - State of Affairs - VISFSAE/FSAE2. Datev eG, Nürnberg, August 2011.

Mendler, M. (2011) A simply-typed calculuis for semantic knowledge bases: Curry-Howard for constructive modal logics. Intuitionistic Modal Logics and Applications (IMLA 2011 associated with CLMPS 2011), Invited talk. Nancy, France, July 25, 2011.

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

Mendler, M. (2012) Durch semantische Datenabstraktion zur problemspezifischen Vollprüfung, 4. Stützpunktveranstaltung, Deggendorfer Forum zur digitalen Datenanalyse (DFDDA), TH Deggendorf, Germany, June 18, 2012.

Sticht, M. (2012) A Game-Theoretic Decision-Procedure for the Constructive Description Logic cALC, 28th British Colloquium for Theoretical Computer Science (BCTCS 2012), Manchester, UK, April 2-5, 2012.

Scheele, S. (2012) Towards Constructive Description Logics, Invited talk, Computer Science Seminar, Dipartimento di Informatica, Università degli Studi di Milano, September 12, 2012.

Scheele, S. (2012) Simply Typed Description Calculus, Invited talk, Computer Science Seminar, Dipartimento di Mathematica e Informatica, Universita' Degli Studi di Udine, September 20, 2012.

Mendler, M. (2012) A simply-typed calculuis for semantic knowledge bases: Curry-Howard for constructive modal logics. Research seminar, Department of Computer Science, University of Stirling, UK, October 7, 2012.

Sticht, M. (2013) A Game-Theoretic Decision-Procedure for the Constructive Description Logic cALC, 4th World Congress and School on Universal Logic (UNILOG'2013), Rio de Janeiro, Brazil, April 3-7, 2013.

Sticht, M. (2013) A Game-Theoretic Decision-Procedure for the Constructive Description Logic cALC, Proof, Computation, Complexity 2013 - Twelfth International Workshop, Toulouse, France, April 22-23, 2013.

Mendler, M. (2014) Curry-Howard for the Constructive Modal Logic CKn, Workshop Logik in der Informatik (LogInf 2014), University of Kassel, Department of Electrical and Computer Engineering, Kassel, November 11, 2014.

• Component-based, functional dataflow architecture for auditing software & domain specific functional programming language for stream-based data processing with applications in financial auditing (FSAE)
• Visual programming interface for data streams (VISFSAE)
• Game-theoretic decision procedure for CKn (cALC)
• Formal proof of confluence of λCKn in the theorem prover Abella
• Implementation of λCK in Haskell using Maps
• Lusterel Library - Combination of Lustre Data Flow and Esterel Control Flow

• DATEV eG, Nürnberg
• dab: Daten - Analysen und Beratung GmbH, Deggendorf 

Michael Mendler,
Email: Send a message to Michael Mendler 

Stephan Scheele,
Email: Send a message to Stephan Scheele