The project has been started together with the Glushkov Institute of Cybernetic and the Kherson State University in 2013.
The legal requirements and laws of different countries of European Union and associated members of EU intersect one with each other during the international financial transactions and agreements. Understanding of legal requirements in the scope of international agreements plays the important role for avoiding of inconsistencies and misuse of ambiguity. Taxation offices and courts of different countries can miss the legal violation or misinterpret the legal case and admit wrong verdict. Different fraud schemes can be hidden and hard to recognize.
One of the way to avoid such issues is the creation of formal model of legal requirements and to provide the corresponding processing and algebraic modeling of legal requirements with the purposes of checking of consistency and compliance of transactions with the laws of corresponding countries.
The main goal of the project is to join together formal methods and contemporary deductive facilities for analysis and processing of the real legal documents. The additional goal is to use formal legal requirements in the simulation of financial transactions and agreements implementation for providing the financial security and avoiding violations and fraud schemes.
It is anticipated that team of law experts and algebraists works with legal requirements documents together for the creation of formal model. The formalization is to transform the behavioral requirements to expressions of behavior algebra and non-behavioral statements as first-order logic axioms. The general purpose of the project is to create the technology of manual, semi-manual or automatic methods of formalization. The corresponding assistant software will be created for automatic purposes. The technology should include the usage of world legal ontology and transforming the acknowledge into algebraic specifications. The result is the set of models of legal requirements presented as behavior algebra specifications.
The created formal model of legal requirements is the input for algebraic programming system or other deductive tools. In the scope of the algebraic system, the number of properties could be checked. There are the properties of consistency and completeness of legal requirements items, compliance with the legal documents of the high level of abstractions especially Constitution.
All this shall be implemented in computations of algebraic systems.
The specific of algebraic research is that we face with big data and big complexity with specific formalization. So, all powerful modern algebraic methods like invariant generation, IC3 technology, approximation methods shall be applied. The corresponding specific technology for modeling and processing of legal requirements shall be set based on the possibilities of the algebraic system.
Concept of “Digital Taxation Office”
It is anticipated the creation of an experimental network of clients that communicate with algebraic systems. Clients perform the different financial transactions and conclude the agreements. The agreements between clients created in the algebraic form like the formalization of legal requirements. The algebraic system with the formal model of Tax Code and other regulations check transactions and agreements for compliance and detect the violation.
Financial Security
Usage of formal methods can avoid and detect the schemes of fraud. Different known cases of fraud shall be formalized as algebraic specifications and system could detect such cases in the transaction. The search of such cases is implemented as resolving of equations in behavior algebra. One of the intentions of such research is combining of the system with cryptocurrency market.
The project is in progress and will be continued in the scope of Horizon 2020.
For more detail, see our conference paper (presentation):