FUB First-order deontic-alethic logic (FODAL)

From ONTORULE Show Case

FODAL is a first-order deontic-alethic logic with sound and complete axiomatization that captures the desired semantics of and interaction between business rules. Satisfiability in FODAL logic may be reduced to a standard first-order satisfiability for a class of formulas restricted to atomic modal sentences that may be used to express the majority of real-world rules. In the attempt to overcome undecidability of FODAL which follows from undecidability of first-order logic, it has been showed that under further restrictions FODAL satisfiability problem may be reduced to that of satisfying some formula in the ALCQI description logic.

Quick references:

• Dmitry Solomakhin, Logical Formalization of Semantic Business Vocabulary and Rules. MSc thesis, Faculty of Informatics, Vienna University of Technology, [1], 2011.
• D. Solomakhin, E. Franconi, and A. Mosca. Logic-based reasoning support for SBVR. In Proceedings of the 26th Italian Conference on Computational Lo- gic (CILC2011), Pescara, Italy, 31 August 31-2 September, 2011, number 810 in CEUR Workshop Proceedings, Aachen, Germany, 2011. Sun SITE Central Europe.