<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta>
      <journal-title-group>
        <journal-title>Tel:</journal-title>
      </journal-title-group>
    </journal-meta>
    <article-meta>
      <title-group>
        <article-title>USE OF METODS OF ALGEBRAIC PROGRAMMING FOR THE FORMAL VERIFICATION OF LEGAL ACTS</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Volodymyr Peschanenko</string-name>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Maksim Poltorackiy</string-name>
        </contrib>
      </contrib-group>
      <volume>38</volume>
      <issue>050</issue>
      <fpage>109</fpage>
      <lpage>114</lpage>
      <abstract>
        <p>This article briefly describes the programmable tool for the analysis of a normative legal document. A mechanism for checking legal requirements is presented. The model of the legal document is proposed in the form of a set of special rules. Verification is provided by means of algebraic programming and methods of symbolic transformation. This approach allows us to analyze the legislative base of structural and logical errors, check the contradictions, completeness and integrity of legal acts. Presently, the mechanism of claster analysis of text, which makes it possible to identify the frequency of occurrence of various vague language constructs.</p>
      </abstract>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>Introduction</title>
      <p>The regulatory framework is prone to frequent changes, the recently enacted laws may contradict existing laws,
which may lead to possible wrong verdicts.</p>
      <p>The situation is also possible when two laws with different consequences can be used for a single legal case. An
example of such a legal case is a precedent: "Convicted or a precedent in favor of a taxpayer". A large number of
crossreferences between normative legal acts makes the analysis of the legislative base of Ukraine more complicated.</p>
      <p>The formalization of laws and the use of methods for formal verification of the model of legal acts is one of the
ways to solve this problem. To create a formal model, formal languages are used that can be used to formalize
information in different areas. However, the possibility of using this arsenal in the processing of legal documents is
significantly reduced. Any official language used to formalize a legal text should operate with legal terms (obligations,
permits, prohibitions). The complexity of this method – the process of formalization – is a rather lengthy process and
requires the interaction of two specialists: a specialist in law and a knowledge engineer (specialist in information
technology).</p>
      <p>The issue of the possibility of using expert systems in legal activities was repeatedly noted by many authors,
discussions on this issue have been conducted since the 60s of the twentieth century. Most expert legal systems are
built on general legal provisions that must be structured and represented in such a system; the functioning of systems
related to the following problems:
- problems of transferring knowledge from human experts to a computer system;
- the problems of submission of knowledge, that is, reconstruction of an array of knowledge in a particular area of
law and its presentation as a structure of knowledge;</p>
      <p>- problems of the use of legal knowledge.</p>
      <p>Next, consider expert systems and methods of presenting legal information.
1. CASE-LAW MODEL</p>
      <sec id="sec-1-1">
        <title>1. Legal search system The Shyster system is based on case law. Uses a case-law model for presenting legal texts. The functionality of this expert system can be divided into two parts:</title>
        <p>2. System of legal analysis. An important feature of this system is the ability to provide certain legal conclusions
and arguments for the lawyer.</p>
        <p>The laws are presented in the form of a specialized specification language. The main idea of this system is based
on a case-law description of legal cases, that is, there is a knowledge base in the system.</p>
        <p>The system considers existing cases and on the basis of old judgments will try to predict the outcome of a new
case. An important feature of this system is the ability to provide certain legal conclusions and arguments for the lawyer.
This system is positioned as a decision support system for lawyers. There is no functional possibility of verification of
legal norms.</p>
        <p>2. PLANNING AND CALCULATION OF STRATEGIES</p>
        <p>
          Expert system TAXADVISER [
          <xref ref-type="bibr" rid="ref11">1</xref>
          ], used in the taxation process. This system is based on certain mathematical
functions and strategies that the lawyer has already formulated on the basis of legal materials.
        </p>
        <p>This approach is based on the planning and calculation of strategies that were obtained by legal experts. The
peculiarity of the approach in this system is the use of the strategy that the lawyer expert provided.
3. LOGICAL PROGRAMMING</p>
        <p>In these expert systems, a model is used that is built on the basis of a certain number of rules of the type:
IF</p>
      </sec>
      <sec id="sec-1-2">
        <title>THEN.</title>
        <p>A set of rules is called a "search space", it is compared with a set of facts. In logical programming it is supposed to
search for the correspondence of a condition to facts and on the basis of "direct" or "reverse" output reach a certain
logical conclusion. This technology is also used by the following systems: Schlobohm, LEX.</p>
        <p>4. XML AND XQUERY LANGUAGE</p>
        <p>
          Also, interesting attempts were made to develop a model of a normative legal document in the form of an xml
document, which in turn would allow using the XQuery language to process this type of document [
          <xref ref-type="bibr" rid="ref12 ref13">2, 3</xref>
          ]. American
scientists tried to present regulatory legal acts in the GJXDM format, the main problem of this approach is the creation of
a certain specification that clearly defined the structure of this legal information. The architecture of the normative legal
act was presented in terms of an xml document with a strictly distinguished dictionary of names collected in the GJXDM
object-oriented information model.
        </p>
        <p>Such an approach did not give an opportunity to analyze normative legal acts, but only allowed to implement the
mechanism of requests for processing a document of this type.</p>
        <p>5. DEONTIC AND FUZZY LOGIC</p>
        <p>Interesting approaches for presenting the legal text and further use in jurisprudence for legal reasoning was the
decision to use deontic and indistinct logic.</p>
        <p>
          The representative of the deontic approach was the speech LLD, which was based on the principles of deontic
logic and had certain advantages for legal application in the field of legal argumentation. LLD, tried to present legal laws
in graphic terms and used indistinct categories that are inherent in this logic [
          <xref ref-type="bibr" rid="ref14">4</xref>
          ].
        </p>
        <p>(Own O1 (Actor A) (Property P)),</p>
        <p>(Own ’Own-2
(Actor ’John) (Property ’Book-3)),
(Own - (Actor ’John)
(Property ’Book-3))</p>
        <p>
          Atomic Formula in LLD language [
          <xref ref-type="bibr" rid="ref14">4</xref>
          ]
        </p>
        <p>The approach using indistinct logic is another attempt to move from very approximate terms that are used in legal
texts to clear terms that are inherent in logic and can be further computer processed.</p>
        <p>6. ONTOLOGY IN LAW
One should also mention the concept of building a model of a legal document using the concept of anthologies.</p>
        <p>The basic concept of anthologies can be used to represent normative legal acts in the form of owl-files, this
structure will allow to implement more complex textual queries and use the concept of SemanticQuery.</p>
        <p>Each of the approaches to constructing a formal model of a normative legal act is quite interesting and has certain
advantages, but none makes it possible to verify the formal properties of the model of legal requirements and analyzed
the legislative basis for logical and structural errors.</p>
        <p>The program that we are developing will provide an opportunity to analyze the legal framework and solve the
following problems:
•</p>
        <p>Checking the legal framework for structural and logical correctness;</p>
        <p>Checking the rule of law for the presence of contradictions in the formation of the regulatory framework.</p>
        <p>Check the model of laws for the completeness of the description and the integrity of the model.</p>
        <p>This program will not only provide an opportunity to check the existing legal and regulatory framework, but also
analyze the new laws that will be added. The application architecture can be represented as follows:</p>
      </sec>
      <sec id="sec-1-3">
        <title>Figur. HLD-scheme of GUI</title>
        <p>Let's briefly consider the main components of the program:
jUCM editor receives jucm-file with an .xml extension, this file is for creating a UCM diagram.</p>
        <p>The validator processes the BAP files, and then returns the BAP file diagnostics.</p>
        <p>3. MSC Viewer – graphical display of MSC chart elements. Graphically displays instances, conditions,
alternatives, altas, akshyns, messages between instances.</p>
        <p>4.</p>
        <p>Insertion Model Editor (IME) – A custom editor for creating basic protocols.</p>
        <p>5. Statistic – a module that will provide an opportunity to look at the descriptive characteristics of laws, see
what structural components affect the outcome of the applicability or inapplicability of this law.</p>
        <p>At the heart of the approach for calculating the effect, we will use ogit., Probit. model and displayed on a special
structural diagram. Also, in the statistics module there is the possibility of isolating the body of knowledge of the source
text, as well as the possibility of constructing a cluster analysis of the text, building a dendrogram of the original legal
text.</p>
        <p>Using a combination of such approaches will make it possible not only to verify structurally logical errors, but
also to evaluate the text of the regulatory framework from the point of view of static text analysis. Such an approach will
make it possible to more effectively use quantitative methods, especially attention is paid to identifying the frequency and
distribution of individual language structures or their groups, as well as stochastic dependencies between them or
between groups of such designs.</p>
        <p>
          To identify structural and logical errors, as well as to check the regulatory framework for formal properties:
inconsistency, completeness and integrity of the model, methods and technologies of insertion modeling (IM) are used.
Next, consider the concept of using IM technology as the main approach for presenting the legal framework, as well as
submitting its verification. The main feature of our approach is the use of methods of symbolic transformations and
algebraic programming in the IM system. Inresertion modeling was developed at the V.M. Glushkov Institute of
Cybernetics [
          <xref ref-type="bibr" rid="ref15">5</xref>
          ].
        </p>
        <p>The basic concept of insertion modeling can be used to interpret the legislative base. Laws can be considered as
standard requirements for functioning. Firms, entrepreneurs and governance can act as agents, various legislative bodies
impose certain requirements on the functioning of agents in the environment. The type of agent that represents the
taxpayer can have the following attributes: name, tax payer status, tax payment regime. In the case of fraud and various
processes over time, a timer and a global clock will be used. The global clock will be used for restrictions related to the
implementation of actions, and the timers will be used to process requests for legal requirements. The behavior of the
system can be described as a system of basic protocols. The basic protocol is the expression</p>
        <p>
          x (U(x) → &lt;P&gt;V(x)),
where U(x) – is the premise that determines the state when the protocol can be applied, V(x) – post condition, which
determines the transition of the system to a new state, P – is the process that illustrates this transition. The basic idea of
the theory of basic protocols is set out in a system that is specified, represented as a composition of agents and
media[
          <xref ref-type="bibr" rid="ref16">6</xref>
          ].
        </p>
        <p>
          The environment is an agent that has a immersion function. The environment is a set of &lt;E, C, A, Inc&gt;, where E –
is the set of environmental states, C – is the set of actions of the environment, A – is the set of actions of agents that are
immersed in the medium, F (A) – is the complete behavior algebra of the agent with the set of behaviors and Ins : E × F
(A) → E – immersion function. Thus, some "Е" environment admits an immersion of any agent with the set of
actions"A" [
          <xref ref-type="bibr" rid="ref17">7</xref>
          ].
        </p>
        <p>The taxpayer can be represented in the system of insertion modeling in the following form:
agent TaxPayer : obj (</p>
        <p>Activity : obj (</p>
        <p>Code : int,
VATpayer : bool,
……
)
Register:obj(</p>
        <p>Voluntary:bool,
Must:bool,
Perfomed:bool,</p>
        <p>TotalIncome : int,
)
……
)</p>
        <p>Using the basic principles of insertion modeling, it is possible to present legal requirements in the form of basic
protocols, and axioms of insertion modeling. Let's consider a fragment of the normative legal act that defines the
requirements for the VAT payer of Ukraine. For convenience of formalization of the normative legal act, we will present
the text in the form of an if-then rule. Then the rule will look like this:</p>
        <p>Rule: If "A person is not a registered taxpayer and for the past 12 months, a person has received an income of
more than 1,000,000, then the person must register as a VAT taxpayer".</p>
        <p>This statement can be written in the IMS in the following way (since in the text of the law the fact of a certain
action is traced, formalization is represented as a basic protocol):</p>
      </sec>
      <sec id="sec-1-4">
        <title>Next we will consider a fragment of the text, Law180.</title>
        <p>Having considered the interpretation of the law, it is not difficult to understand that the requirement for a taxpayer
can be interpreted by a sequence of logical operations (conjunctions, disjunctions and equivalence), since at the clause of
law 180 the fact of action is not formally indicated, then the formalization is performed as inertial modeling axioms. We
give an example of the axiom from the law 180:
</p>
        <p>A180_1_1 &lt;=&gt;
(((x.commercialActivity.status = GONNA_BE) |/ (x.commercialActivity.status = DOES)) &amp;
(x.registrationVAT.status =</p>
        <p>DOES) &amp;x.registrationVAT.decisionVoluntaryVAT))
 art_180_1_2 &lt;=&gt;
(x.registrationVAT.necessity |/ (x.registrationVAT.status = DID)
....
</p>
        <p>A180_1_5 : (A180_1_5 &lt;=&gt; (x.otherActivity = CONTROL_ESTATE))
Then completely a fragment of the law, can be interpreted as follows (as a certain logical sequence of axioms):
 art_180_1 &lt;=&gt; (x.TaxPayer &lt;=&gt; (art_180_1_1 |/ art_180_1_2 |/... |/ art_180_1_5)).</p>
        <p>This approach can be applied to the entire tax code of Ukraine, but in the process of formalization we found the
following laws, the text of which is quite difficult to present in a formalized form, because their design can be interpreted
in different ways. In the following we consider the following laws:
186.1. The place of supply of goods shall be:
186.2.1. the place of actual supply of services related to movable property, namely:
 ancillary services in transportation activity: loading, unloading, reloading, warehouse pro- cessing of goods
and other similar services;</p>
        <p>
           actual location of services in culture, art, education, science, sport, entertainment or other similar services,
including without limitations services by organizers of activities in the said areas and services provided for organization
of paid exhibitions, conferences, scientific workshops and other similar events [
          <xref ref-type="bibr" rid="ref18">8</xref>
          ].
        </p>
        <p>The construction of these laws is a counter-version, formulations like: or other, etc. are difficult to interpret with
formal languages.</p>
        <p>In order to formalize such a law, it is necessary to clearly understand what are similar services within the
framework of Article 180, paragraph 180.2.1. The time given for the development of adequate formalization within these
laws should clearly interpret the meaning of this expression, because in this form the meaning can be subjective.</p>
      </sec>
    </sec>
    <sec id="sec-2">
      <title>Conclusions</title>
      <p>In this article, briefly describes the functionality of the program based on methods and techniques of insertion
modeling. The technology of presenting legal information using IMS technology is described.</p>
      <p>An important feature of this approach is the use of this technology for formal verification of the legal framework.
This approach makes it possible to use the IMS methodology to check the regulatory framework on: inconsistency,
completeness and curative.</p>
      <p>The use of methods of cluster analysis of text provides a unique opportunity to assess the initial tex of the
regulatory framework in terms of static text analysis.</p>
      <p>The possibility of isolating the knowledge base of the normative legal base document and the methods of cluster
analysis will make it possible to use quantile methods more effectively to determine the frequency of individual
language constructions or groups of such constructions.</p>
      <p>Proceeding from the analyzed literature, I want to emphasize that not one of the technologies makes it possible to
analyze the test of a normative legal document for such a wide class of problems. Already at the initial formalization
process, you can analyze and identify weaknesses in the regulatory base of Ukraine. The implementation of such a tool
is solved by the following class of tasks:
•</p>
      <p>Review of regulatory legal documents on the possibility of revealing formal and logical errors.</p>
      <p>Construction and verification of the normative legal document model for contradictions, completeness and
• Analysis of the text of the source document to determine the frequency of the appearance of ambiguous
language text constructs, as well as highlight the body of knowledge of the source text.</p>
      <p>This program module will give an opportunity to elicit controversial constructions of the legislative base of
Ukraine, to identify possible structural and logical errors, as well as possible contradictory constructions in the
legislative framework.</p>
      <p>•
integrity.
Література</p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          <string-name>
            <surname>Michaelsen R.H.</surname>
          </string-name>
          <year>1984</year>
          .
          <article-title>An expert system for federal tax planning</article-title>
          .
          <source>Expert Systems</source>
          ,
          <volume>1</volume>
          (
          <issue>2</issue>
          ). P.
          <volume>149</volume>
          -
          <fpage>167</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          <string-name>
            <surname>Peychev</surname>
            <given-names>V.</given-names>
          </string-name>
          <year>2004</year>
          .
          <article-title>XML model for legal documents</article-title>
          . Problems of Engineering Cybernetics and Robotics. 54. P.
          <volume>86</volume>
          -
          <fpage>91</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          <string-name>
            <surname>Peychev</surname>
            <given-names>V.</given-names>
          </string-name>
          <year>2005</year>
          .
          <article-title>Legal document - a formal model. Problems of Engineering Cybernetics</article-title>
          and Robotics. 55. P.
          <volume>64</volume>
          -
          <fpage>70</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          <string-name>
            <surname>McCarty L.T.</surname>
          </string-name>
          <year>1989</year>
          ,
          <article-title>May. A language for legal Discourse I. basic features</article-title>
          .
          <source>In Proceedings of the 2nd international conference on Artificial intelligence and law (P</source>
          .
          <fpage>180</fpage>
          -
          <lpage>189</lpage>
          ). ACM.
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          <string-name>
            <given-names>Letichevsky A.A.</given-names>
            ,
            <surname>Letychevskyi</surname>
          </string-name>
          <string-name>
            <given-names>O.A.</given-names>
            and
            <surname>Peschanenko</surname>
          </string-name>
          <string-name>
            <surname>V.S.</surname>
          </string-name>
          <year>2011</year>
          , June.
          <article-title>Insertion modeling system</article-title>
          .
          <source>In International Andrei Ershov Memorial Conference on Perspectives of System Informatics (P</source>
          .
          <fpage>262</fpage>
          -
          <lpage>273</lpage>
          ). Springer, Berlin, Heidelberg.
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          <string-name>
            <given-names>Letichevsky A.</given-names>
            ,
            <surname>Kapitonova</surname>
          </string-name>
          <string-name>
            <surname>J.</surname>
          </string-name>
          ,
          <string-name>
            <given-names>Letichevsky</given-names>
            <surname>Jr</surname>
          </string-name>
          .A.,
          <string-name>
            <surname>Volkov</surname>
            <given-names>V.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Baranov</surname>
            <given-names>S.</given-names>
          </string-name>
          and
          <string-name>
            <surname>Weigert</surname>
            <given-names>T.</given-names>
          </string-name>
          <year>2005</year>
          .
          <article-title>Basic protocols, message sequence charts, and the verification of requirements specifications</article-title>
          .
          <source>Computer Networks</source>
          ,
          <volume>49</volume>
          (
          <issue>5</issue>
          ). P.
          <volume>661</volume>
          -
          <fpage>675</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          <string-name>
            <given-names>Letichevskii A.A.</given-names>
            ,
            <surname>Kapitonova</surname>
          </string-name>
          <string-name>
            <given-names>Y.V.</given-names>
            ,
            <surname>Volkov</surname>
          </string-name>
          <string-name>
            <given-names>V.A.</given-names>
            and
            <surname>Vyshemirskii</surname>
          </string-name>
          <string-name>
            <surname>V.V.</surname>
          </string-name>
          <year>2003</year>
          .
          <article-title>Insertion programming</article-title>
          .
          <source>Cybernetics and Systems Analysis</source>
          ,
          <volume>39</volume>
          (
          <issue>1</issue>
          ). P.
          <volume>16</volume>
          -
          <fpage>26</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          <string-name>
            <surname>Ukrainy P.K. Tax Code</surname>
          </string-name>
          of Ukraine] vid
          <volume>02</volume>
          .12.
          <year>2017</year>
          ,
          <article-title>(zi zminamy i dopovnenniamy)</article-title>
          .
          <source>zakon4. rada. gov. ua.</source>
        </mixed-citation>
      </ref>
      <ref id="ref9">
        <mixed-citation>
          <string-name>
            <surname>Popple J.</surname>
          </string-name>
          <year>1996</year>
          .
          <article-title>A pragmatic legal expert system</article-title>
          .
          <source>Dartmouth (Ashgate).</source>
        </mixed-citation>
      </ref>
      <ref id="ref10">
        <mixed-citation>
          10.
          <string-name>
            <surname>Michaelsen</surname>
            <given-names>R.H.</given-names>
          </string-name>
          <year>1984</year>
          .
          <article-title>An expert system for federal tax planning</article-title>
          .
          <source>Expert Systems</source>
          ,
          <volume>1</volume>
          (
          <issue>2</issue>
          ). P.
          <volume>149</volume>
          -
          <fpage>167</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref11">
        <mixed-citation>
          1.
          <string-name>
            <surname>Michaelsen</surname>
            <given-names>R.H.</given-names>
          </string-name>
          <year>1984</year>
          .
          <article-title>An expert system for federal tax planning</article-title>
          .
          <source>Expert Systems</source>
          ,
          <volume>1</volume>
          (
          <issue>2</issue>
          ). P.
          <volume>149</volume>
          -
          <fpage>167</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref12">
        <mixed-citation>
          2.
          <string-name>
            <surname>Peychev</surname>
            <given-names>V.</given-names>
          </string-name>
          <year>2004</year>
          .
          <article-title>XML model for legal documents</article-title>
          . Problems of Engineering Cybernetics and Robotics. 54. P.
          <volume>86</volume>
          -
          <fpage>91</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref13">
        <mixed-citation>
          3.
          <string-name>
            <surname>Peychev</surname>
            <given-names>V.</given-names>
          </string-name>
          <year>2005</year>
          .
          <article-title>Legal document - a formal model. Problems of Engineering Cybernetics</article-title>
          and Robotics. 55. P.
          <volume>64</volume>
          -
          <fpage>70</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref14">
        <mixed-citation>
          4.
          <string-name>
            <surname>McCarty L.T</surname>
          </string-name>
          .
          <year>1989</year>
          ,
          <article-title>May. A language for legal Discourse I. basic features</article-title>
          .
          <source>In Proceedings of the 2nd international conference on Artificial intelligence and law (P</source>
          .
          <fpage>180</fpage>
          -
          <lpage>189</lpage>
          ). ACM.
        </mixed-citation>
      </ref>
      <ref id="ref15">
        <mixed-citation>
          5.
          <string-name>
            <surname>Letichevsky</surname>
            <given-names>A.A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Letychevskyi</surname>
            <given-names>O.A.</given-names>
          </string-name>
          and
          <string-name>
            <surname>Peschanenko</surname>
            <given-names>V.S.</given-names>
          </string-name>
          <year>2011</year>
          , June.
          <article-title>Insertion modeling system</article-title>
          .
          <source>In International Andrei Ershov Memorial Conference on Perspectives of System Informatics (P</source>
          .
          <fpage>262</fpage>
          -
          <lpage>273</lpage>
          ). Springer, Berlin, Heidelberg.
        </mixed-citation>
      </ref>
      <ref id="ref16">
        <mixed-citation>
          6.
          <string-name>
            <surname>Letichevsky</surname>
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kapitonova</surname>
            <given-names>J.</given-names>
          </string-name>
          ,
          <string-name>
            <given-names>Letichevsky</given-names>
            <surname>Jr</surname>
          </string-name>
          .A.,
          <string-name>
            <surname>Volkov</surname>
            <given-names>V.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Baranov</surname>
            <given-names>S.</given-names>
          </string-name>
          and
          <string-name>
            <surname>Weigert</surname>
            <given-names>T.</given-names>
          </string-name>
          <year>2005</year>
          .
          <article-title>Basic protocols, message sequence charts, and the verification of requirements specifications</article-title>
          .
          <source>Computer Networks</source>
          ,
          <volume>49</volume>
          (
          <issue>5</issue>
          ). P.
          <volume>661</volume>
          -
          <fpage>675</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref17">
        <mixed-citation>
          7.
          <string-name>
            <surname>Letichevskii</surname>
            <given-names>A.A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kapitonova</surname>
            <given-names>Y.V.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Volkov</surname>
            <given-names>V.A.</given-names>
          </string-name>
          and
          <string-name>
            <surname>Vyshemirskii</surname>
            <given-names>V.V.</given-names>
          </string-name>
          <year>2003</year>
          .
          <article-title>Insertion programming</article-title>
          .
          <source>Cybernetics and Systems Analysis</source>
          ,
          <volume>39</volume>
          (
          <issue>1</issue>
          ). P.
          <volume>16</volume>
          -
          <fpage>26</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref18">
        <mixed-citation>
          8.
          <string-name>
            <surname>Ukrainy P.K. Tax Code</surname>
          </string-name>
          of Ukraine] vid
          <volume>02</volume>
          .12.
          <year>2017</year>
          ,
          <article-title>(zi zminamy i dopovnenniamy)</article-title>
          .
          <source>zakon4. rada. gov. ua.</source>
        </mixed-citation>
      </ref>
      <ref id="ref19">
        <mixed-citation>
          9.
          <string-name>
            <surname>Popple</surname>
            <given-names>J.</given-names>
          </string-name>
          <year>1996</year>
          .
          <article-title>A pragmatic legal expert system</article-title>
          .
          <source>Dartmouth (Ashgate).</source>
        </mixed-citation>
      </ref>
      <ref id="ref20">
        <mixed-citation>
          10.
          <string-name>
            <surname>Michaelsen</surname>
            <given-names>R.H.</given-names>
          </string-name>
          <year>1984</year>
          .
          <article-title>An expert system for federal tax planning</article-title>
          .
          <source>Expert Systems</source>
          ,
          <volume>1</volume>
          (
          <issue>2</issue>
          ). P.
          <volume>149</volume>
          -
          <fpage>167</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref21">
        <mixed-citation>
          Kherson State University, Str. Universytets'ka,
          <volume>27</volume>
          ,
          <fpage>73000</fpage>
          ,
          <string-name>
            <surname>Kherson</surname>
          </string-name>
          , Ukraine.
        </mixed-citation>
      </ref>
      <ref id="ref22">
        <mixed-citation>
          <string-name>
            <surname>Tel</surname>
          </string-name>
          : +
          <volume>38</volume>
          (
          <issue>095</issue>
          ) 324
          <fpage>1557</fpage>
          .
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>