Links to Formal Logic

Abstract

This chapter deals with how to relate languages in this book to formal logics. The convention in the chapter is that a formal theory, or simply a theory, is a name for a set of formulas with no free variables in some formal logic. So how can you map (parts of) models to theories, and why should we do so? Relationships between requirements modeling languages and formal logics are a recurrent topic in requirements engineering. In KAOS, theories in linear temporal first-order logic are themselves parts of models. The same in Tropos. The motivation is that you can take a model in a requirements modeling language and map (parts of) it to a theory in some formal logic, in order to answer questions that your requirements modeling language could not. I will look at two among many topics on the relationships between requirements modeling languages and formal logics. I restrict the discussion to one formal logic, namely classical propositional logic (CPL), and discuss the following. 1. How to map a model to a CPL theory if every fragment equates to an atomic proposition. (Sect. 15.2) 2. How to map a model to CPL theory, if every fragment maps to a conjunction of formulas of classical propositional logic. (Sect. 15.3) 3. What can be the risks of mapping models to theories. (Sect. 15.4)