Annotation

Annotation: Requirements in regulatory documents are often stated in natural language, which makes the automatic detection of contradictions between them difficult. Moreover, the existence of a contradiction may depend on the document version, the operating mode of the object, exceptions, and the priorities of other requirements. The aim of this article is to define the requirements for a formal model suitable for the automated detection of such contradictions and to propose a model based on these requirements. The paper presents a comparative analysis of normative logics, temporal logics, goal-oriented models, and specialized normative languages. The main result is the DDLLTLf formalism, in which norms are represented as temporal obligations with exceptions and priorities, while the problem of detecting contradictions is reduced to SAT checking. The scientific novelty lies in combining a logic of norms with exceptions and a temporal logic over finite traces within a unified semantics of prevailing norms, as well as in proving a Boolean encoding of this semantics. The practical significance of the approach lies in its potential use as an intermediate representation layer between the text of a regulatory document and a solver, enabling the detection of real conflicts between regulatory requirements.