<!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 />
    <article-meta>
      <title-group>
        <article-title>Reasoning over Knowledge Graphs in an Intuitionistic Description Logic?</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Bernardo Alkmim</string-name>
          <email>bpalkmim@gmail.com</email>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Edward Haeusler</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Daniel Schwabe</string-name>
          <email>dschwabe@inf.puc-rio.br</email>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Departamento de Informa ́tica</institution>
          ,
          <addr-line>Pontif ́ıcia Universidade Cato ́lica do Rio de Janeiro</addr-line>
          ,
          <country country="BR">Brazil</country>
        </aff>
      </contrib-group>
      <abstract>
        <p>In this work we present a way to model and reason over Knowledge Graphs via an Intuitionistic Description Logic called iALC. We also introduce a Natural Deduction System for iALC to reason over our modelling of the information of the Knowledge Graphs. Furthermore, we apply this modelling to some examples in a context that aims to support the concepts of Trust, Privacy, and Transparency.</p>
      </abstract>
      <kwd-group>
        <kwd>Description Logic</kwd>
        <kwd>Intuitionistic Logic</kwd>
        <kwd>iALC</kwd>
        <kwd>Knowledge Graphs</kwd>
        <kwd>Natural Deduction</kwd>
      </kwd-group>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>1 Introduction</title>
      <p>
        Throughout the years there have been several different ways to represent knowledge,
either by trying to mimic human cognitive behaviour or by other approaches.
Knowledge Base Systems (KBSs) [
        <xref ref-type="bibr" rid="ref13">13</xref>
        ] are one of such methods, derived from Expert Systems,
explained in [
        <xref ref-type="bibr" rid="ref5">5</xref>
        ] and [
        <xref ref-type="bibr" rid="ref10">10</xref>
        ].
      </p>
      <p>
        One way to represent KBSs is via Knowledge Graphs (KGs), which can be seen in
[
        <xref ref-type="bibr" rid="ref15">15</xref>
        ] and [
        <xref ref-type="bibr" rid="ref18">18</xref>
        ]. With their graph-like structure, KGs offer a versatile way to represent
data that postpones the necessity for a schema, which adapts well to different domains.
The fact that they are graphs is, as well, another positive point, since this
mathematical structure has extensive literature and theory [
        <xref ref-type="bibr" rid="ref4">4</xref>
        ] behind it. This is especially useful
when one utilises Machine Learning, since KGs can connect it to Knowledge
Representation thus imbuing it with tools to solve certain questions in the data, such as Data
Insufficiency or Zero-shot Learning.
      </p>
      <p>
        One other way to represent knowledge is via the usage of Description Logics (DL)
[
        <xref ref-type="bibr" rid="ref2">2</xref>
        ]. DLs consist in the representation of entities called concepts, roles, and individuals,
as well as their relationships, based around axioms. This type of Logic comes in
different flavours, depending on which properties one wishes to utilise. One of the attractive
points of DLs is the possibility to make syntactic reasoning (due to being a Logic) over
the associated KB, via whichever deduction system is more adequate.
      </p>
      <p>
        There is, as well, especially for the domain of Law, the option of utilising Deontic
Logic, but it is criticised (as in [
        <xref ref-type="bibr" rid="ref19">19</xref>
        ], for instance) for not making explicit the models and
? The authors gratefully acknowledge financial support from CNPq.
theories for the making of legal KBSs, among other reasons. By choosing Description
Logic, one may utilise a calculus for deductions, similarly to Deontic Logic, but without
facing the same modelling issues.
      </p>
      <p>We then end up with two means to represent data: KGs, which are versatile and can
represent data more accurately, and DLs, over which one can reason while extracting
more direct meaning from the reasoning itself at the same time. Due to their equivalence
in representation, we are able to reap the good parts of both these methods over the same
KBS.</p>
      <p>In this article, we present our efforts in translating a representation of a KBS that
focuses on the concepts of Trust, Privacy, and Transparency of information from a KG
to a DL, namely, iALC, in order to reason over it.</p>
      <p>
        iALC is a Logic that has been used to represent and reason over the domain of Law,
and its structure is based on Kelsenian Jurisprudence. Thus, legal individuals can be
seen as Valid Legal Statements (VLSs) in iALC, and the notion of precedence between
Laws (as per Theory of Legal Order in [
        <xref ref-type="bibr" rid="ref3">3</xref>
        ]) can be directly represented in it as a relation
between worlds in a Kripke Model. The choice to utilise a Description Logic instead of
a type of the more usual Deontic Logic comes from the existence of certain conceptual
problems of Deontic Logic, especially when one considers the notion of validity of a
normative sentence.
      </p>
      <p>In section 2, we introduce the concept of KGs and the framework which allows
them to better deal with concepts of Trust, Privacy, and Transparency of information.</p>
      <p>In section 3, we explain the main concepts of the DL we choose to reason with,
iALC, and explain why it was chosen to do so.</p>
      <p>In section 4, we contextualise the KBS and give some examples of formalizations
in iALC and the reasonings made, as well as discuss our decision making throughout
this process.</p>
      <p>In section 5, we conclude the article and point to future directions of this work.</p>
      <p>In the appendix A, we present the Natural Deduction system rules created for iALC
to make the deduction itself.
2</p>
    </sec>
    <sec id="sec-2">
      <title>Knowledge Graphs</title>
      <p>
        There are multiple different definitions for KGs in the literature and varied
implementations of them (all discussed thoroughly in [
        <xref ref-type="bibr" rid="ref12">12</xref>
        ]), but they all share a central idea: they
utilise graphs to represent data and knowledge. The concept comes from the 70s [
        <xref ref-type="bibr" rid="ref16">16</xref>
        ],
but the term itself has been popularised by Google in 2012,1 when they implemented
the concept to create a system to support moving from search to question answering.
      </p>
      <p>In general, the nodes in a KG represent entities of the real world and the edges,
relations between them. This is, however, a rather simplistic approach that is not much
different from a labelled graph. In order to talk about knowledge, it is necessary to have
a supplementary ontology, or a set of rules of the domain to be represented. One may
use quantification of variables, as well as separate one big KG into smaller ones, in
order to isolate semantically certain parts of the original graph.
1 https://www.blog.google/products/search/introducing-knowledge-graph-things-not/</p>
      <p>
        In [
        <xref ref-type="bibr" rid="ref17">17</xref>
        ], the authors present a framework called KG Usage, which allows KGs to
support Trust, Transparency, and Privacy concerns in its modelling. This allows for
usage in applications for whom decisions based on security or disclosure of information
of knowledge is important.
3
      </p>
      <p>
        iALC
Description Logics (DL) were already proposed for semantic analysis of natural
language utterances in [
        <xref ref-type="bibr" rid="ref6">6</xref>
        ]. In [
        <xref ref-type="bibr" rid="ref7">7</xref>
        ] the DL iALC [
        <xref ref-type="bibr" rid="ref9">9</xref>
        ] was used as the basis of a solver/reasoner
for the questions in the exam. iALC is based on the canonical ALC, and was by
definition made to deal with law systems. In it, valid legal statements (VLS) are not
propositions, but individuals in a legal ontology, i. e. one law cannot be true or false, it just
either exists or not in a concept. The propositions we consider are some of the
concepts of the ontology (i. e. concepts of the form a : C or C v D, for a nominal and C,
D concepts), which represent the legal systems that can hold different kinds of laws.
They also have a precedence relationship, derived by the hierarchy of individual laws
of Kelsenian Jurisprudence [
        <xref ref-type="bibr" rid="ref14">14</xref>
        ]. As an example, one can imagine Brazilian Law or
other similar system. It has the Constitution, comprised of some general principles that
must precede every other (usually more specific) law that is based on or created after
it. With this notion, one can create different tiers of laws in order to not generate legal
antinomies with the laws of higher tiers, and those higher laws must precede the lower
ones.
      </p>
      <p>
        In [
        <xref ref-type="bibr" rid="ref1">1</xref>
        ] iALC is utilised to model and solve questions from the OAB Exam.2 In this
article, the characteristics of this logic are more thoroughly explained, especially in how
they make it well suited to deal with normative sentences, especially laws.
      </p>
      <p>In general, in iALC, legal individuals are specific combinations of laws that
represent an artificial legal being, which can validate or not certain concepts. They do not,
however, represent fully individuals outside of the legal expressiveness of the logic; they
are mere legal projections of real-life concepts. For example, john : Attorney states that
the legal individual john, which represents a legal document that proves that John is
an attorney, is part of the concept Attorney, which represents the set of laws relating to
attorneys. In general, to simplify, individuals like john are assumed to always be, from
the start, in a nominal.3 Notice that everything in this example is in the ontology on
laws.</p>
      <p>
        iALC is also an intuitionistic logic. Intuitionistic logic is constructive by nature [
        <xref ref-type="bibr" rid="ref11">11</xref>
        ].
Intuitionistically, :A being true can be understood as there being no way to construct a
proof of A (or that, by assuming A to be true, one is led to a contradiction). With this,
we have, for instance, that ::A being true does not imply in A being true, which is a
valid implication in classical logic. In fact, intuitionistic logic is weaker than classical
logic (see [
        <xref ref-type="bibr" rid="ref11">11</xref>
        ]), but it allows for non-conflicting existence of otherwise
thought-tobe contradictory logical formulas in Description Logic, particularly. In the domain of
2 The Brazilian Bar Exam, which candidates have to pass in order to be able to practice law.
3 A nominal is a concept defined extensionally, consisting of only one individual, by which it is
referenced. A nominal for john is f johng. Throughout this article we will omit this notation,
referring to the nominals without the brackets.
law, this allows, for instance, the existence of a model representing two distinct legal
systems, one in which the death penalty is not allowed, and the other in which it is not.
In a regular (i.e. Classical) DL, this cannot be represented directly when modelling,
since a Kripke model for a Classical Logic collapses all worlds (the legal individuals)
to the same one, causing a contradiction by allowing and prohibiting the death penalty
at the same time. This would force us to find a more conflated way to insert Legal
Individuals into the logic, at the risk of losing legibility, and, even worse, soundness.
      </p>
      <p>This non-conflicting existence of different sets of rules relates directly to the
existence of different KGs in section 4, each with their own set of rules, which may
contradict those of other KGs. iALC not only allows for those to coexist, but it also has means
to solve those apparent contradictions.
4</p>
    </sec>
    <sec id="sec-3">
      <title>Some Examples</title>
      <p>
        The examples utilised here are from [
        <xref ref-type="bibr" rid="ref17">17</xref>
        ], further explained in the third section of that
article. To summarise, in a fictional context a disaster occurs and a person, Ed, wishes
to donate to a foundation in order to give aid to the people affected by it. He, however,
wants to be sure that his money will be well spent, so he needs to trust the organisation
to which he intends to give his money. There is another person, George, who is an officer
in a non-governmental organisation (NGO) called ReliefOrg, whom Ed does not trust.
Assuming that there is a law that requires NGOs to disclose publicly (transparency)
their officers, Ed must have access to this information from ReliefOrg. Even so, George
may not want to disclose his personal information to others (right to privacy), creating
a conflict that must be resolved. In this case, since it is in the law that this kind of
information must be disclosed, the transparency law has priority.
      </p>
      <p>The approach there postulates the existence of a trusted graph containing all the
statements an agent will rely upon to decide to take some action. Rules define when a
statement should be included in this graph (trust), as well as when some action should
be allowed (transparency) or denied (privacy). In the example, there are also other
scenarios in this same context that relate the concepts of Trust, Privacy, and Transparency
in similar ways.</p>
      <p>It is worth noting that this hierarchy of normative sentences, i.e. rules, laws, was the
starting point to formalise this information in iALC, since the logic was created to deal
with laws from the cradle.</p>
      <p>
        We will now show a modelling of basic information and some examples of rules of
this scenario, based on the same rules from the original article, that modelled them in a
KG divided in several Knowledge Items, each one being a nanopublication [
        <xref ref-type="bibr" rid="ref8">8</xref>
        ].
4.1
      </p>
      <sec id="sec-3-1">
        <title>Base knowledge</title>
        <p>Part of the information is shared by all agents, and is the base knowledge for the
scenario, namely: ReliefOrg is a non-profit organisation, AuditInc is a certification agency,
George is an officer of ReliefOrg and of AuditInc.</p>
        <p>For the base graph knowledge, we have the following formulas:
relie f : NonPro f itL
audit : CertAgencyL
NonPro f it v OrganisationL
CertAgency v OrganisationL
george o f f icerInOrg relie f
george o f f icerInOrg audit</p>
        <p>In the formulas above, we can see that the individuals are represented by nominals
in iALC, as would be expected. We utilise a concept to represent a category or set.
In the first formula, we have that the individual relie f , an individual representing
ReliefOrg, is part of the concept NonPro f it, a concept for non-profit organisations. One
concept can be a subset of another, as in the third formula, which states that non-profit
organisations are a subset of organisations in general. When a relation between two
individuals in established, it is translated into a role. In the fifth formula, for example, the
role o f f icerInOrg relates the individuals george and relie f .</p>
        <p>To model the rules in iALC, we needed to make them somewhat general to be able
to chain formulas with one another. So, we used generic labels when modelling e.g.
relie f : NonPro f itL, where L is any list of labels for the concept NonPro f it.</p>
        <p>To make the actual reasoning, we developed a Natural Deduction (ND)4 system
for iALC (whose rules are all in appendix A), which has labels to facilitate the
chaining of existential restrictions. Our ND system needs these chainings in order to
connect in the same reasoning individuals that are related indirectly (via transitivity) in
a fully TBOX-esque fashion. For instance, when an agent intends to do an action to
an organisation that has a certain o f f icer, we need to encapsulate all these different
relations between distinct agents in one single formula in order to make more direct
and structurally simple reasonings without losing meaning. Luckily, it is possible in
DLs via applying restrictions sequentially on concepts. The labels on concepts also aid
this chaining by giving the context at all times, thus maintaining the soundness of the
system. This chaining of formulas is explained more concretely in section 4.2.</p>
        <p>The rules utilised in this document are, mostly, 9 intro, 9 elim, v elim, and
u intro. If applicable, the versions of the rules are the ones that have nominals.</p>
        <p>The rules used have to do with our modelling choices: most of the modelling
involved existential restrictions (9), subjunctions of concepts (v), and conjunctions of
concepts (u). Also, since the cases are always instantiated, all the rules involved
nominals, to reflect the information as faithfully as possible.
4.2</p>
      </sec>
      <sec id="sec-3-2">
        <title>Rule Ed1 (TRUST)</title>
        <p>We begin with the first rule of knowledge graph for the agent Ed: Ed wants to donate to
a certified not-for-profit organisation. More precisely, if an organisation org has (some)
officer o f , financial record f in, f in is audited by organisation aud, aud is certified
by organisation cert, cert is a Certification Agency and the provenance graph for cert
includes the fact that it is an accredited agency, then Ed’s trusted graph includes the fact
4 ND is a deduction system that has many similarities to the way a person makes an actual
deduction, which relates closely to a previous usage of iALC: answering questions to a Bar
Exam. It is, in a way, a more readable Sequent Calculus. Another reason in its favour is the
lack of support in general of inferential tools to Intuitionistic Logics.
that org is a non-profit organisation. Some of those sentences can be represented with
role assertions, creating the related roles:
f in auditedBy aud
aud certi f iedBy cert
org hasFinRecord f in
o f o f f icerInOrg org</p>
        <p>These formulas, however, do not fit well into our Natural Deduction system, since
they involve information pertinent to the ABOX (assertion) part of iALC, and the ND
system reasons over the TBOX (terminological) part of it. Luckily, they are equivalent
to a more TBOX-friendly format, in the form of Restrictions of Concepts (in our case,
existential restrictions).5 We have not yet seen the case in which a universal restriction
was necessary, but their modelling would be similar and would chain just as naturally
as the existential ones (and iALC supports it if needed). This results in:
f in : 9auditedBy:OrganisationL
aud : 9certi f iedBy:CertAgencyL
org : 9hasFinantialRecord:FinRecordL
o f : 9o f f icerInOrg:OrganisationL</p>
        <p>The formulas are given generic labels (namely L, representing a list of labels) in
order to give them flexibility when used in proofs, because, in those, they need to be able
to represent any context in which they appear. Once context is given, L is substituted
by an adequate list of labels. This generic list of labels can be interpreted as the
formula being valid regardless of the context in which it is inserted. The supposition that
financial record f in is audited by an organisation, i.e. 9auditedBy:Organisation, can be
used in the situation presented, or in any other. If we use fixed labels for this context,
the isolated sentence may lose meaning in a different context (maybe one without a
certification agency involved, for instance). After the proof, these concrete contexts will
be explained more clearly. By chaining some of those in order to relate these different
individuals we have:
f in : 9auditedBy:9certi f iedBy:CertAgencyL</p>
        <p>The formula above represents a refinement in f in : 9auditedBy:OrganisationL via
aud : 9certi f iedBy:CertAgencyL, which is an existential restriction on CertAgency, a
subconcept of Organisation.</p>
        <p>org : 9hasFinRecord:9auditedBy:9certi f iedBy:OrganisationL</p>
        <p>This last formula can be read as org has a (certain) financial record which is audited
by an organisation certified by a certification agency, which is itself an organisation.
Representing the entire rule, we have:
9hasFinRecord:9auditedBy:9certi f iedBy:Organisation v NonPro f itL
Showing that, for Ed’s graph, a company that fits into these criteria must be a
nonprofit organisation. So, here is the proof for the first rule in our ND system (names were
shortened to fit the page):
5 The choice here is between universal and existential restrictions, but universal restrictions
would imply that, for instance, the organisation org would have every financial record (in the
world) related to it, which is very rarely the case.
cert : Acc Acc v CA
cert : CA
v e</p>
        <p>v e
org : NP
9h:9a:9c:O v NP
v e</p>
        <p>In this proof, the generic label L is substituted by the concrete labels, giving the
context needed to the formulas. For instance, f in : 9a:9c:O9h has the label 9h,
indicating that the restricted concept 9a:9c:O can be even further restricted via the role h
(hasFinantialRecord), which connects f in to another individual, namely, org. Whereas
org : 9h:9a:9c:O has no labels, because they are not necessary. In the case of this
formula, everything is explicit in the restrictions themselves.</p>
        <p>It is worth noting that, in our situation, o f can be replaced by george, org by relie f ,
and cert, by audit, showing that ed is aware that relie f is a non-profit organisation.
4.3</p>
      </sec>
      <sec id="sec-3-3">
        <title>Rule Ed2 (Ed does not trust George)</title>
        <p>To capture the fact that Ed does not trust George (in the sense of donating to an
organisation where George is an officer), we include the following rule. If Ed’s trusted graph
includes the fact that org is a non-profit organisation, George is officer of org, and Ed
intends to take action a of type Donate to org, then a is Denied.</p>
        <p>We can set the formulas to:
george : 9o f f icerInOrg:OrgL
org : NonPro f itL
act : DonateL
act : 9directedTo:OrgL
ed : 9intends:DonateL
(alternatively) ed : 9intends:9directedTo:OrgL
We want to get to act : DeniedL.</p>
        <p>However, before going on to the proof, we need a formalisation of the fact that Ed
does not trust George as an officer in an organisation, and that it nullifies his action:
ed notTrust george, which becomes ed : 9notTrust:PersonL, and, after another
transformation:
ed : 9notTrust:9o f f icerInOrg:OrgL</p>
        <p>We have just inserted a new concept, Person, not necessarily present in the
context, which was necessary in order to categorise of what concept george is a part. An
analogous concept would be O f f icer, but the name would be solely to give semantic
information to the reader. To the situation itself the semantics of the concepts are given
extensionally.</p>
        <p>We also need to account for the fact that the action is directed towards a non-profit
organisation:
(9intends:9directedTo:NonPro f it u 9noTrust:9o f f icerIn:Org)
v 9intendsTo:DeniedL</p>
        <p>Then, we have the following proof:
org : NP9i;9d
act : 9d:NP9i 9 i
ed : 9i:9d:NP 9 i ed : 9nT:9o:O
ed : (9i:9d:NP u 9nT:9o:O)
u i</p>
        <p>(9i:9d:NP u 9nT:9o:O) v 9i:DL
ed : 9i:D
act : D9i 9
e
v e
4.4</p>
      </sec>
      <sec id="sec-3-4">
        <title>Rule George1 (PRIVACY)</title>
        <p>Now, let us focus on the graph of George, the officer, who has a rule that does not
allow divulging (reading) any information about him, including his association with
an organisation. This rule, which represents his right to privacy, and rule 4.5, which
represents the transparency of a non-profit organisation are apparently in conflict. In
the next sections we explain how this conflict is solved. The proofs for the rules of his
graph will be similar to those in the graph of Ed.</p>
        <p>If george is an officer of organisation org, action a is of type read, and Agent ag
intends a Then a is Denied.</p>
        <p>org : OrgL
george o f f icerIn org, aka george : 9o f In:OrgL
a : ReadL
ag intends a, aka ag : 9intends:ReadL
a directedTo george, aka a : 9directedTo:9o f f icerIn:OrgL</p>
        <p>We also have, by the privacy rule, that (9intends:9directedTo:9o f f icerIn:Org u
9intends:Read) v 9intends:Denied.</p>
        <p>We want to arrive at a : DeniedL.</p>
        <p>The proof is as follows:
org : O9in;9diTo;9o f In
g : 9o f In:O9in;9diTo 9 i
a : 9diTo:9o f In:O9in 9 i a : R9in
ag : 9in:9diTo:9o f In:O 9 i ag : 9in:R 9 i
ag : (9in:9diTo:9o f In:O u 9in:R) u i</p>
        <p>(9in:9diTo:9o f In:O u 9in:R) v 9in:D
ag : 9int:D
a : D9int 9 e
v e</p>
        <p>To contextualise, org is the organisation relie f , and the agent who intends to read
information on ReliefOrg, ag, is ed.
4.5</p>
      </sec>
      <sec id="sec-3-5">
        <title>Rule Transp (TRANSPARENCY)</title>
        <p>The rule for the Transparency ruling over our agent George’s privacy rule is: if an
organisation org is of type NonPro f it and has officer o f , action a is of type read and
an agent ag intends a, then A is Allowed.</p>
        <p>There are also two additional pieces of information to the graph: the primary source
to the transparency rule is Non-profit Act, and Non-profit Act is a Law.
org : NonPro f itL
o f f o f f icerIn org, which becomes o f f : 9o f f icerIn:NonPro f itL
act : ReadL
act directedTo org, which becomes act : 9directedTo:NonPro f itL
ag intends act, which becomes ag : 9intends:ReadL, and later
ag : 9intends:9directedTo:NonPro f itL</p>
        <p>By transparency, (9intends:9directedTo:9o f f icerIn:NonP u 9intends:Read) v
9intends:Allowed. We also may represent l : NonPro f itAct as the legal individual for
the Non-profit Act. With that, we should have act : AllowedL.</p>
        <p>This will not be used in the proof, but it is interesting to state the disjunction between
the concepts Denied and Allowed: Denied v :Allowed.</p>
        <p>org : NP9in;9diTo;9o f In
o f r : 9o f In:NP9in;9diTo 9 i
a : 9diTo:9o f In:NP9in 9 i
ag : 9in:9diTo:9o f In:NP 9 i
ag : (9in:9diTo:9o f In:NP u 9in:R)
a : R9in
ag : 9in:R 9 i</p>
        <p>u i (9in:9diTo:9o f In:NP u 9in:R) v 9in:A
ag : 9int:A
a : A9int 9 e
v e</p>
        <p>Also, we have a secondary proof to show that the transparency rule (represented by
the individual rtr) is preceded by the law l.</p>
        <p>rtr : (9in:9diTo:9o f In:NP u 9in:R) v 9in:A l
rtr
l : (9in:9diTo:9o f In:NP u 9in:R) v 9in:A
elim</p>
        <p>This Natural Deduction rule, elim, is a way to introduce the mechanism of
precedence between individual laws directly into the Natural Deduction system. The
smaller premise, l rtr, indicates the precedence among the individuals concerned.
The bigger premise taking to the conclusion tells us that, since a concept is valid for
an individual who is preceded by another, the one who precedes (in our case, l) must
also validate such concept, due to the intuitionistic nature of the logic, that requires the
construction of the validity of a concept to be passed through (in this case, to have been
passed through) to following individuals hierarchically.</p>
        <p>At this point, we still need to relate rules 4.4 and 4.5, which could pose a
problem since they apparently contradict each other. The following rule, then, comes to the
rescue.
4.6</p>
      </sec>
      <sec id="sec-3-6">
        <title>MetaRule1 (Precedence)</title>
        <p>This rule simply states that Laws precede personal privacy rules from the graphs of
agents, such as rule 4.4.</p>
        <p>This is simply solved by iALC with LegalRule v PersonalPrivRuleL.</p>
        <p>We can, then, conclude that rule 4.5 has precedence over rule 4.4, since the law
ruling over the transparency of non-profit organisations has precedence over George’s
right to privacy (at least when regarding his work at such an organisation).
In this article, we presented the concepts of KGs and showed how they can be used
in contexts that involve the concepts of Trust, Privacy, and Transparency, as well as an
alternate formalisation for them in iALC, an Intuitionistic Description Logic, to show
one way one can reason over them. This modelling and reasoning was proven successful
on the context shown and conveyed how we can translate the complexities of KGs via
the intuitionistic notion of truth that iALC has.</p>
        <p>For future work, we intend to extend this representation in iALC in this context of
Trust, Privacy, and Transparency, specially since a lot of the decision making in terms
of reasoning comes from the relations between laws that seem conflicting at first glance,
but that are solved by mechanisms iALC is equipped to model.</p>
        <p>In regards to the more theoretical side of the work, we aim to give a more formal
introduction to the Natural Deduction system for iALC, via showing its properties of
soundness and completeness, for instance, which are out of the scope of this article, and
possibly implement an automated reasoner to it for it to be used in a larger scale.</p>
      </sec>
    </sec>
    <sec id="sec-4">
      <title>Natural Deduction System for iALC</title>
      <p>Let a and b concepts, x and y nominals, d formula, and R a role. L represents a list of
labels (possibly empty). Labels represent either negations of concepts, or universal or
existential restrictions on concepts, made implicit. They indicate a sort of context to the
concept they are attached to. L8 is a list that restricts all labels in itself to 8R of some
kind, and L9 restricts all to 9R. Rules that utilise nominals and involve x and y assume
that there is a role connecting them, i.e. xRy. Please note that only the rules related
to iALC operators utilised in this article are shown. The n in the names of some rules
indicate that those are the versions which utilise nominals.</p>
      <p>y : a 9R;L
x : (9R:a )L 9
intro
x : (9R:a )L
y : a 9R;L
9
elim
x : (a L1 v b L2) v
intro
n
x : a L1
x : (a L1 v b L2)
x : b L2
v
elim
n</p>
      <p>Alkmim et al.</p>
      <p>x : aL
.
.
.</p>
      <p>.
x : x(::a?):L : intro n
x : aL x : (:a):L
x : ?
? intro n
x : aL8 x : b L8
x : (a u b )L8 u intro n
x : (a u b )L8
x : aL y x
y : aL
x : (a u b )L8</p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1.
          <string-name>
            <given-names>Bernardo</given-names>
            <surname>Alkmim</surname>
          </string-name>
          , Edward Hermann Haeusler, and
          <string-name>
            <given-names>Alexandre</given-names>
            <surname>Rademaker</surname>
          </string-name>
          .
          <article-title>Utilizing ialc to formalize the brazilian oab exam</article-title>
          .
          <source>In Proceedings from the EXplainable AI in Law Workshop (XAILA)</source>
          .
          <source>CEUR-WS</source>
          ,
          <year>2018</year>
          . http://ceur-ws.
          <source>org/</source>
          Vol-
          <volume>2381</volume>
          /.
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          2.
          <string-name>
            <given-names>Franz</given-names>
            <surname>Baader</surname>
          </string-name>
          , Diego Calvanese, Deborah
          <string-name>
            <surname>Mcguinness</surname>
            ,
            <given-names>Daniele</given-names>
          </string-name>
          <string-name>
            <surname>Nardi</surname>
          </string-name>
          , and
          <string-name>
            <surname>Peter PatelSchneider. The Description Logic Handbook: Theory</surname>
          </string-name>
          , Implementation, and
          <string-name>
            <surname>Applications</surname>
          </string-name>
          . Cambridge University Press; 2nd Edition, 01
          <year>2007</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          3.
          <string-name>
            <given-names>N.</given-names>
            <surname>Bobbio and M.C.C.L. dos Santos</surname>
          </string-name>
          . Theory of Legal Order. Ed. Universidade de Bras´ılia,
          <year>1995</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          4.
          <string-name>
            <given-names>J.A.</given-names>
            <surname>Bondy</surname>
          </string-name>
          and
          <string-name>
            <given-names>U.S.R</given-names>
            <surname>Murty</surname>
          </string-name>
          .
          <source>Graph Theory</source>
          . Springer Publishing Company,
          <source>Incorporated, 1st edition</source>
          ,
          <year>2008</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          5.
          <string-name>
            <surname>Bruce</surname>
            <given-names>G</given-names>
          </string-name>
          .
          <article-title>Buchanan and Edward A. Feigenbaum. Dendral and meta-dendral: Their applications dimension</article-title>
          .
          <source>Artificial Intelligence</source>
          ,
          <volume>11</volume>
          (
          <issue>1</issue>
          ):
          <fpage>5</fpage>
          -
          <lpage>24</lpage>
          ,
          <year>1978</year>
          .
          <article-title>Applications to the Sciences and Medicine</article-title>
          .
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          6.
          <string-name>
            <given-names>Cleo</given-names>
            <surname>Condoravdi</surname>
          </string-name>
          , Dick Crouch, Valeria de Paiva, Reinhard Stolle, and Daniel G. Bobrow.
          <article-title>Entailment, intensionality and text understanding</article-title>
          .
          <source>In Proceedings of the HLT-NAACL 2003 Workshop on Text Meaning - Volume</source>
          <volume>9</volume>
          ,
          <string-name>
            <surname>HLT-</surname>
          </string-name>
          NAACL-TEXTMEANING '
          <volume>03</volume>
          , pages
          <fpage>38</fpage>
          -
          <lpage>45</lpage>
          , Stroudsburg, PA, USA,
          <year>2003</year>
          .
          <article-title>Association for Computational Linguistics</article-title>
          .
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          7.
          <string-name>
            <given-names>Pedro</given-names>
            <surname>Delfino</surname>
          </string-name>
          , Bruno Cuconato, Edward Hermann Haeusler, and
          <string-name>
            <given-names>Alexandre</given-names>
            <surname>Rademaker</surname>
          </string-name>
          .
          <article-title>Passing the brazilian oab exam: Data. Legal Knowledge and Information Systems</article-title>
          , page
          <volume>89</volume>
          ,
          <year>2017</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          8.
          <string-name>
            <given-names>Paul</given-names>
            <surname>Groth</surname>
          </string-name>
          , Andrew Gibson, and
          <string-name>
            <given-names>Johannes</given-names>
            <surname>Velterop</surname>
          </string-name>
          .
          <article-title>The anatomy of a nano-publication</article-title>
          .
          <source>Information Services and Use</source>
          ,
          <volume>30</volume>
          , 01
          <year>2010</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref9">
        <mixed-citation>
          9. Edward Hermann Haeusler and
          <string-name>
            <given-names>Alexandre</given-names>
            <surname>Rademaker</surname>
          </string-name>
          .
          <article-title>On how kelsenian jurisprudence and intuitionistic logic help to avoid contrary-to-duty paradoxes in legal ontologies</article-title>
          .
          <source>Proc. Journal of Applied Non-Classical Logics</source>
          ,
          <year>2016</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref10">
        <mixed-citation>
          10.
          <string-name>
            <surname>Frederick</surname>
          </string-name>
          Hayes-Roth,
          <article-title>Donald A</article-title>
          .
          <string-name>
            <surname>Waterman</surname>
          </string-name>
          , and
          <string-name>
            <surname>Douglas</surname>
            <given-names>B.</given-names>
          </string-name>
          <string-name>
            <surname>Lenat</surname>
          </string-name>
          .
          <source>Building Expert Systems. Addison-Wesley Longman Publishing Co., Inc., USA</source>
          ,
          <year>1983</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref11">
        <mixed-citation>
          11.
          <string-name>
            <given-names>A.</given-names>
            <surname>Heyting</surname>
          </string-name>
          .
          <source>Intuitionism: An Introduction. North-Holland Publishing, Amsterdam, Netherlands, 3rd edition</source>
          ,
          <year>1956</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref12">
        <mixed-citation>
          12.
          <string-name>
            <surname>Aidan</surname>
            <given-names>Hogan</given-names>
          </string-name>
          , Eva Blomqvist, Michael Cochez, Claudia d'Amato, Gerard de Melo, Claudio Gutierrez, Jose´ Emilio Labra Gayo, Sabrina Kirrane,
          <string-name>
            <given-names>Sebastian</given-names>
            <surname>Neumaier</surname>
          </string-name>
          , Axel Polleres, Roberto Navigli,
          <string-name>
            <surname>Axel-Cyrille Ngonga</surname>
            <given-names>Ngomo</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Sabbir M. Rashid</surname>
          </string-name>
          , Anisa Rula, Lukas Schmelzeisen, Juan Sequeda,
          <string-name>
            <surname>Steffen Staab</surname>
            , and
            <given-names>Antoine</given-names>
          </string-name>
          <string-name>
            <surname>Zimmermann</surname>
          </string-name>
          .
          <source>Knowledge graphs</source>
          ,
          <year>2020</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref13">
        <mixed-citation>
          13.
          <string-name>
            <surname>Matthias</surname>
            <given-names>Jarke</given-names>
          </string-name>
          , Bernd Neumann, Yannis Vassiliou, and
          <string-name>
            <given-names>Wolfgang</given-names>
            <surname>Wahlster</surname>
          </string-name>
          .
          <source>KBMS Requirements of Knowledge-Based Systems, page 381-394</source>
          . Springer-Verlag, Berlin, Heidelberg,
          <year>1989</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref14">
        <mixed-citation>
          14. H. Kelsen.
          <source>Pure Theory of Law. Lawbook Exchange</source>
          ,
          <year>2005</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref15">
        <mixed-citation>
          15.
          <string-name>
            <surname>Maximilian</surname>
            <given-names>Nickel</given-names>
          </string-name>
          , Kevin Murphy, Volker Tresp, and
          <string-name>
            <given-names>Evgeniy</given-names>
            <surname>Gabrilovich</surname>
          </string-name>
          .
          <article-title>A review of relational machine learning for knowledge graphs</article-title>
          .
          <source>Proceedings of the IEEE</source>
          ,
          <volume>104</volume>
          , 12
          <year>2015</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref16">
        <mixed-citation>
          16.
          <string-name>
            <given-names>E. W.</given-names>
            <surname>Schneider</surname>
          </string-name>
          and VA. Human Resources Research Organization, Alexandria. Course Modularization Applied [microform] :
          <article-title>The Interface System and Its Implications For Sequence Control</article-title>
          and
          <string-name>
            <given-names>Data</given-names>
            <surname>Analysis</surname>
          </string-name>
          / E. W. Schneider. Distributed by ERIC Clearinghouse [Washington, D.C.],
          <year>1973</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref17">
        <mixed-citation>
          17. Daniel Schwabe and
          <string-name>
            <given-names>Carlos</given-names>
            <surname>Laufer</surname>
          </string-name>
          .
          <article-title>Trust and privacy in knowledge graphs</article-title>
          .
          <source>CoRR</source>
          , abs/
          <year>1903</year>
          .07673,
          <year>2019</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref18">
        <mixed-citation>
          18.
          <string-name>
            <surname>Stephan</surname>
            <given-names>Seufert</given-names>
          </string-name>
          , Patrick Ernst,
          <string-name>
            <given-names>Srikanta J.</given-names>
            <surname>Bedathur</surname>
          </string-name>
          , Sarath Kumar Kondreddi, Klaus Berberich, and
          <string-name>
            <given-names>Gerhard</given-names>
            <surname>Weikum</surname>
          </string-name>
          .
          <article-title>Instant espresso: Interactive analysis of relationships in knowledge graphs</article-title>
          .
          <source>In Jacqueline Bourdeau</source>
          , Jim Hendler, Roger Nkambou, Ian Horrocks, and Ben Y. Zhao, editors,
          <source>Proceedings of the 25th International Conference on World Wide Web, WWW</source>
          <year>2016</year>
          , Montreal, Canada,
          <source>April 11-15</source>
          ,
          <year>2016</year>
          , Companion Volume, pages
          <fpage>251</fpage>
          -
          <lpage>254</lpage>
          . ACM,
          <year>2016</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref19">
        <mixed-citation>
          19.
          <string-name>
            <given-names>Andre</given-names>
            <surname>Valente</surname>
          </string-name>
          and
          <string-name>
            <given-names>Joost</given-names>
            <surname>Breuker</surname>
          </string-name>
          .
          <article-title>A model-based approach to legal knowledge engineering</article-title>
          .
          <source>JURIX</source>
          ,
          <year>1992</year>
          , 01
          <year>1992</year>
          .
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>