Consultation to Effectiveness and Logical Meaning
Susumu Yamasaki
a
and Mariko Sasakura
b
Department of Computer Science, Okayama University, Tsushima-Naka, Okayama, Japan
Keywords:
Abstract Consultation, Causal Analysis, Abstract State Machine, Model Theory in Database.
Abstract:
This paper deals with consultation as a role of consultant like a teacher in a virtual reality class for lessons.
The consultation subject is taken in causal analysis and database design to conceive causal relation. The causal
analysis is abstracted into effectiveness which is caused by requisites and prohibitions for effects. The database
design is represented as recursive Backus-Naur Form for structural expressions. Then abstract consultation
can be regarded as a function to transform effectiveness into recursive representation. The sense or meaning
of such abstract consultation may be a semantics of conditioned formulas in modal logic. The modal logic
is formulated in this paper, by extending postfix modality for name of database design as well as greatest
fixed point operator for denoting an equilibrium state set where the transformation of effectiveness with prefix
modality to design with postfix modality may be available. The conditioning of formulas is given by a state set
so that the formula may be considered in terms of propositional base. As regards recursive representations in
Backus-Naur Form for database design, model theory is established in 3-valued domain, for the sense of strong
negation in accordance to prohibitions influencing effectiveness. Some fixed point is taken for the mapping
associated with recursive representations, where the mapping is related to formations of models over 3-valued
domain. The fixed point model can be seen as means of retrieval. However, because the mapping is generally a
nonmonotonic function whose fixed point semantics is not always available, we have another method to adopt
negation as failure for strong negation such that the model of a given recursive representation as database
is always guaranteed if the representation takes a restricted form. Abstract consultation to effectiveness for
database design is thus formulated, with model theory in database representations.
1 INTRODUCTION
Based on the views on cognitive managements, we
try to deal with complexity of systems by simplifi-
cations to abstract formality. For expertise in human
computer interaction, we here consider the function of
consultant abstracted from a teacher in a virtual real-
ity class of lessons, as consultation from causal anal-
ysis to design of database. As backgrounds to study
abstract consultation for formality to simplify com-
plexity in refined technologies, we have seen knowl-
edge engineering refinements:
(i) Causal analysis with reasoning is fundamen-
tal, from knowledge engineering aspects (R. Reiter,
2001). It is objective knowledge for action that forms
computational structure of designs to implement com-
plex knowledgeable systems.
(ii) Nonmonotonic logic should be the subject for
knowledge, even with respect to temporality (Hanks
a
https://orcid.org/0000-0001-7895-5040
b
https://orcid.org/0000-0002-8909-9072
and McDermott, 1987).
(iii) Knowing is the subject to be formalized widely
and rigidly (Kooi, 2016; Naumov and Tao, 2019).
The consultation is in this paper taken as a pro-
cess. The idea to think of processes is related to ab-
stract state machine and process algebra (R. Milner,
1999):
(i) Rewriting process with reductions for calculus is
formulated in functionalism as in C. Bertolissi et al.
(2006).
(ii) Mobile ambients are dealt with in process of
behaviours (Cardelli and Gordon, 2000; Merro and
Nardelli, 2005).
(iii) The compositions of transitions in automata
are formulated in algebraic structures (Droste et al.,
2009).
Following knowledge engineering, process alge-
bra concepts and the idea on autonomy (Yamasaki
and Sasakura, 2020), the purpose of this paper is to
abstract the role of a consultant as a teacher of vir-
tual reality class. The knowledge engineering views
extract a consultation function from a causal analysis
Yamasaki, S. and Sasakura, M.
Consultation to Effectiveness and Logical Meaning.
DOI: 10.5220/0010977400003197
In Proceedings of the 7th International Conference on Complexity, Future Information Systems and Risk (COMPLEXIS 2022), pages 57-64
ISBN: 978-989-758-565-4; ISSN: 2184-5034
Copyright
c
2022 by SCITEPRESS – Science and Technology Publications, Lda. All rights reserved
57
of effects to recursive relation for design of database
whose manipulations implement the effects conceived
in causal analysis.
As regards effectiveness, computability or logi-
cal reasonability is the primary concept already estab-
lished. In accordance with effects conceived in causal
analysis, effectiveness is here captured as causal re-
lations between requisites with prohibitions and ef-
fects. The design of database follows effective-
ness, where recursive causal relation is transferred to
the design and representation by Backus-Naur Form
for database. The transition or transformation from
causal analysis to design can be understood in abstract
state machine or transition systems as interpretations
for modal logic.
In modal logic, so many works are compiled.
Among them, modal logic with fixed point operator
(Dam and Gurov, 2002; Kozen, 1983; Venema, 2008)
is significant for this paper, since the denotational se-
mantics, that is, senses or meanings of consultation
require fixed point operator. In this paper, for a non-
trivial sense to be provided, the greatest fixed point is
needed. The actions as behaviors are treated in modal
logic (Giordano et al., 2000; Spalazzi and Traverso,
2000), where the consultation of this paper is an ab-
stract action from behavioral senses, so that this work
is relevant to modal logic achievements on actions.
First-order modal logic (Fitting, 2002) and topologi-
cal space in transition systems for modal logic (Gold-
blatt and Hodkinson, 2020) are to be kept in mind to
the next step of advancements. In this paper for a sim-
ple outlook on, a primary step to denotation of ab-
stract consultation is made in the propositional base,
by means of postfix modality for design (action), and
by fixed point (for causal analysis followed by design)
as an equilibrium.
The paper is organized as follows. Section 2 is
concerned with an example of the consultant in a vir-
tual reality class, whose role would be an abstract
consultation. The consultation involves causal re-
lation analysis for design of database to implement
causal relation. In Section 3, modal logic is prepared
by taking postfix modality for representation of the
design by name, and greatest fixed point for denota-
tion of abstract consultation. Section 4 gives recursive
representation of (database) design for causal analy-
sis by Backus-Naur Form. The model theory of such
representations are presented in 3-valued domain, for
the effects caused by requisites and prohibitions. The
model theory conceives nonmonotonic function treat-
ments, where some approximate interpretation can be
adopted for prohibited predicates of database. Con-
cluding remarks are mentioned in Section 5.
2 ABSTRACT CONSULTATION
Paying attention to the consultant role of a teacher at a
class to students, we abstract some consultation func-
tion for simplicity rather than for complex organiza-
tion of refined implementation techniques. That is,
simplicity by abstraction from effectiveness for analy-
sis may be transformed to design of a system scheme.
It is regarded as consultation function
• from analysis in problem solving, by effectiveness
in causal relation,
• to (system) design of database, by recursive rep-
resentation.
We have constructed a version of virtual reality class
for lessons, which may implement a partial function
of real-time online class for a teacher to be interactive
with students (M. Sasakura et al., 2021).
(a) Images taken by video camera may be organized
as virtual reality class (VR-class), where students
can take part in the VR-class by the computing
facility.
(b) The images can include not only a teacher with
blackboards but also class mates.
(c) VR-class can include any angle from the point of
video camera shots. Several blackboards in a class
may be observed.
(d) Some zoom up to the blackboard is implemented,
for the student to observe the contents written on.
In the constructed VR-class, a teacher can take a con-
sultant role for analysis of causal relation. Then the
teacher would present a chart to transform the analy-
sis to database, where the transformation is realized as
an abstract process from effectiveness in causal anal-
ysis into recursive Backus Naur Form (for structural
representation of objects), as below.
At Virtual Reality Class:
Teacher — Consultant
Consultation:
Causal Analysis ⇒ Database
Abstract Effectiveness ⇒ Recursive BNF
Effectiveness is historically formulated as in log-
ical frameworks. Even trends are given in studies on
reductions of decidability (Rasga et al., 2021) and on
what an inference is (Tennant, 2021).
In this paper, effectiveness can be captured as fol-
lows, for causal analysis:
COMPLEXIS 2022 - 7th International Conference on Complexity, Future Information Systems and Risk
58
Effects Requisites Prohibitions
Flying Airline In f ected
··· ··· ···
··· ··· ···
For example, Air plane (a predicate) and Not
In f ected (a negated predicate) may cause the Flying
effect (a predicate), and so on.
As a design to realize effectiveness obtained by
analysis, database is a static framework, whose dy-
namic behaviors are implemented as retrieval func-
tions. Such database may be represented by recursive
Backus-Naur Form (BNF), in this paper, where BNF
is of use for structural analysis of recursion. For ex-
ample, a list List over a set of objects Ob can be ex-
pressed in the manner like
L ::= null | cons(a,L)
where:
(a) null denotes the empty list.
(b) a is from Ob, and
(c) cons is a specific function (to take an object fol-
lowed by a list and form an extended list).
In the following sections, recursive BNF and model
theory for database would be made in details.
As a background, such a transformation of ef-
fectiveness (in table) to recursive BNF (as database
descriptions) comes from an algebraic structure of a
bounded lattice, as follows:
Effectiveness =⇒ Recursive BNF
(Based on a Bounded Lattice)
A bounded lattice (As,
W
,
V
,⊥,>) equipped with
the partial order v and an implication ⇒ may be
taken:
(i) ⊥ and > are the least and the greatest elements of
the algebra (set) As, respectively, with respect to the
partial order v.
(ii) The least upper bound ( join)
W
and the greatest
lower bound (meet)
V
exist for any two elements of
As.
(iii) The implication ⇒ (a relation on As) is defined
in a way that z v (x ⇒ y) iff x
V
z v y.
3 MODAL LOGIC TO
REPRESENT CONSULTATION
A motive of this section is to represent the meaning of
consultation made by a consultant as in VR-class. The
consultation is here conditioned by logical formulas
such that the sense or meaning of consultation may
be represented by semantics of logical formulas.
To see some adequate logical framework, consul-
tation is now captured as abstract transformation from
analysis to design, which is conceived in transitions of
abstract state machine or transition system (for model
theory) of modal logic.
With respect to representation of analysis (name),
prefix modality is adopted. As regards representa-
tion of design (name), we take postfix modality. In
addition to postfix modality, fixed point operator is
needed, for consultation to denote a state set in tran-
sition system.
A modal logic with greatest fixed point operator
and with postfix modality is presented, where it may
be modified from modal mu-calculus (Kozen, 1983)
and Henessy-Milner Logic.
The set Ψ of (logical) formulas are defined induc-
tively as follows.
ψ ::= > | p | ¬ψ | ψ ∧ ψ | νX.ψ | [a]ψ | ψ[d]
Note that the intuitive meanings of symbols are
described as below, where the formal meanings are
given with the transition system.
(a) > is the truth.
(b) p denotes propositions.
(c) ∧ stands for the conjunction.
(d) ¬ is the logical negation.
(e) ν is a greatest fixed point operator.
(f) [a] is a prefix modality with analysis label (name)
a.
(g) [d] is a postfix modality with design label (name)
d.
(h) ν is a greatest fixed point operator, with X a propo-
sition variable.
A Transition System S :
For the set Ψ of formulas, a transition system S is
defined to be (S,A,D,Re,Rel,V ) where:
(i) S is a set of states.
(ii) A is a set of labels for analyses.
(iii) D is a set of labels for designs.
(iv) Re maps to each a ∈ A a relation Re(a) on S.
(v) Rel maps to each d ∈ D a relation Rel(d) on S.
(vi) Val : Prop → 2
S
maps to each proposition (vari-
able) a set of states.
Semantic Functions:
A semantic function [[ ]] : Ψ → 2
S
is defined to
regard the semantics of a formula ψ as a subset of S
by [[ψ]].
(a) [[>]] = S.
Consultation to Effectiveness and Logical Meaning
59
(b) [[p]] = Val(p).
(c) [[ψ
1
∧ ψ
2
]] = [[ψ
1
]] ∩ [[ψ
2
]].
(d) [[¬ψ]] = S − [[ψ]].
(e) [[[a]ψ]]
= {s ∈ S | ∀s
0
: (s,s
0
) ∈ Re(a) entails s
0
∈ [[ψ]]}.
(f) [[ψ[d]]]
= {s ∈ S | ∀s
0
: (s
0
,s) ∈ Rel(d) entails s
0
∈ [[ψ]]}.
(g) [[νX.ψ]] = ∪ {T ⊆ S | T ⊆ [[ψ]]
[X:=T]
},
where every occurrence of X in ψ is positive, and
[[ψ]]
[X:=T]
denotes a set obtained from [[ψ]] by sub-
stituting T for any occurrence of X, and ∪ stands
for a union (of sets).
Note for µ-calculus including a least fixed point oper-
ator µ that, with negation sign ¬,
⊥ = ¬>,
ϕ
1
∨ ϕ
2
= ¬(¬ϕ
1
∧ ¬ϕ
2
),
haiϕ = ¬[a]¬ϕ, and
µX.ϕ = ¬νX.¬ϕ[X := ¬X],
where ϕ[X := ¬X] means substituting ¬X for X
in all free occurrences of X in ϕ.
Semantics for Consultation:
What such a VR-class consultant denotes is here
discussed. From the function views, it is regarded as
a transformation, abstracted from consultation for de-
sign with analysis of effects caused by requisites and
prohibitions.
Without concretized data of computing environ-
ments in a state, a state set may denote the sense of
consultation, conditioned by a logical formula.
(a) The state set denoted by [a]ψ is the one which is
regarded as states before applying analysis, caus-
ing state transition to the state set denoted by ψ.
(b) The state set denoted by ψ[d] is the one which is
regarded as states after applying design, causing
state transition from the state set denoted by ψ,
(c) They are both to contain the state sets denoted by
ψ and by a proposition variable X (occurring in
ψ) as consultation denotations.
When an environmental state set of a consultant is
conditioned by a formula φ containing positive occur-
rences of a proposition variable X, the transformation
of analysis a to design d is an abstraction of consulta-
tion, whose semantics may be given as a state set [[X]]
such that
[[X]] = [[[a]φ(X) ∧ φ(X)[d]]],
where φ(X) is just φ with positive occurrences of X.
Because the empty state set
/
0 satisfies this equa-
tion, but too trivial to represent such an environmental
aspect of semantics. Rather than the least fixed point,
we can have a greatest fixed point of the equation,
which can be expressed by ν-operator:
[[νX.[a]φ ∧ φ[d]]]
We may also make use of [[νX.[a]φ]] ∩ [[νX.φ[d]]],
because of Proposition 1.
Proposition 1. We have:
[[νX.[a]ψ ∧ ψ[d]]] ⊆ [[νX .[a]ψ]] ∩ [[νX.ψ[d]]].
Proof. With respect to the greatest fixed point of
monotonic function, we see
[[νX.[a]ψ ∧ ψ[d]]] ⊆ [[νX .[a]ψ]].
Similarly it is seen that
[[νX.[a]ψ ∧ ψ[d]]] ⊆ [[νX .ψ[d]]].
Thus the proposition holds.
4 RECURSIVELY DESCRIBED
DATABASE
The recursive representation transformed from effects
(which are caused by requisites and prohibitions as in
Section 2) is examined, where recursive representa-
tion may induce database. Abstract representation is
firstly given by Backus-Naur Form for effectiveness.
Then model theory is discussed with respect to ab-
stract representation inducing database.
4.1 Abstract Representation
A set of expressions of the form Req; Pro ⇒ E f is
considered, where Req and Pro represent requisites
and prohibitions, respectively, for an effect E f .
It can be described in Backus-Naur Form (BNF),
by recursion.
Rule ::=
/
0 | {rule} ∪ Rule
rule ::= Con ⇒ E f
Con ::= Req; Pro
Req ::= null
Req
| q;Req
Pro ::= null
Pro
| not q : Pro
E f ::= q | not q
where the semicolon are used to stand for concatena-
tions of strings, and:
(a)
/
0 is the empty set in Rule.
(b) null
Req
is the empty sequence in Req and null
Pro
is the empty sequence in Pro, where null
Con
=
null
Req
; null
Pro
is the empty sequence in Con.
(c) q is a variable for predicates.
(d) not is negation sign.
COMPLEXIS 2022 - 7th International Conference on Complexity, Future Information Systems and Risk
60
Concretization of BNF:
This BNF can be concretized as causal relation by
means of logical or algebraic expressions. Each rule
can represent:
q
1
∧ ... ∧ q
n
∧ not r
1
∧ ... ∧ not r
m
→ p
where p is q or not r with the symbols:
(a) q, q
i
(1 ≤ i ≤ n), r, r
j
(1 ≤ j ≤ m) as predicate or
algebraic variables.
(b) ∧ as the logical and or the algebraic meet opera-
tion.
(c) → as logical or algebraic implication.
Rule may denote a logical and or algebraic meet
of rules such that Rule is regarded as causal relation.
3-Valued Model Theory:
Base on 2-valued model domain, answer set pro-
gramming (Gebser and Schaub, 2016) and its appli-
cation to problem solving (Kaufmann et al., 2016) are
established. With the unknown (denoted by “1/2”) as
in 3-valued domain {0,1/2,1}, causal relation should
be made clearer, for data technologies, in abstraction
from logical or algebraic representations.
The domain {0,1/2,1}, with a partial order v:
0 v 0,0 v 1/2,0 v 1,
1/2 v 1/2,1/2 v 1,
1 v 1,
with 0 as the bottom and with 1 as the top, is a
bounded lattice with an implication, as introduced in
Section 2. We here take this 3-valued domain with
model theory in abstracted BNF.
For a given Rule, let
Σ
Rule
= {q | q ∈ Rule}.
It is denoted just by Σ, if the set Rule is clear in the
context.
With an assignment
V : Σ → {0, 1/2,1},
the evaluation of a set Rule is given in conditional
statement form. The conditional statement form is
[v
1
→ e
1
,...,v
n
→ e
n
,e
n+1
] (n ≥ 1),
which is to describe:
if v
1
then e
1
else if v
2
then e
2
···
···
else if v
n
then e
n
else e
n+1
An evaluation function eval with respect to an as-
signment V is recursively defined for a rule set Rule.
The evaluation is similar to the one (Yamasaki and
Sasakura, 2021a), where the cases for evaluations of
expressions are regarded as represented with the con-
ditional statement form.
eval
V
(Rule) =
[∀rule ∈ Rule : eval
V
(rule) = 1 → 1,
∃rule ∈ Rule : eval
V
(rule) = 0 → 0, 1/2]
eval
V
(rule) =
[eval
V
(Con) v eval
V
(E f ) → 1,
eval
V
(E f ) = 0 → 0, 1/2]
eval
V
(Con) =
[∀q ∈ Re : V (q) = 1 and
∀not q ∈ Pro : V (q) = 0 → 1,
∃q ∈ Re : V (q) = 0 or
∃not q ∈ Pro : V (q) 6= 0 → 0, 1/2]
eval
V
(E f ) =
[E f = q → V (q),E f = not q with V (q) = 0 → 1,0]
eval
V
(not q) = [V (q) = 0 → 1, 0]
4.2 Model Theory
We here present model theory for recursively defined
Rule in BNF where there is no case that both forms
Con ⇒ q and Con
0
⇒ not q exist, for some q.
Model Theory:
For a set Rule with an assignment V , let
Pos
V
= {q | V (q) = 1}, and
Neg
V
= {q | V (q) = 0}.
Note that Pos
V
∩ Neg
V
=
/
0, that is, the pair
(Pos
V
,Neg
V
) is consistent. If eval
V
(Rule) = 1, then
the pair form (Pos
V
,Neg
V
) is interpreted as a model
of Rule.
For a rule of the form Con ⇒ E f , Con(rule)
stands for Con and E f (rule) for E f , respectively.
Definition 2. A mapping
Trans : (2
Σ
× 2
Σ
) → (2
Σ
× 2
Σ
)
is defined, such that, with Trans to be applied to
(Pos
V
,Neg
V
), (Pos
V
0
,Neg
V
0
) may be obtained:
(a) If there exists a rule such that Con(rule) = null
Con
or eval
V
(Con(rule)) = 1, E f (rule) is in Pos
V
0
.
(b) If there is no rule with E f (rule) = q and no rule
with E f (rule) = not q, q is in Neg
V
0
.
(c) For any rule with E f (rule) = q such that
eval
V
(Con(rule)) = 0, q is in Neg
V
0
.
(d) If there exists a rule with E f (rule) = not q such
that eval
V
(Con(rule)) 6= 0, q is in Neg
V
0
.
We describe properties of the mapping Trans.
Proposition 3. Assume the mapping
Trans : (2
Σ
× 2
Σ
) → (2
Σ
× 2
Σ
).
Consultation to Effectiveness and Logical Meaning
61
Consistency is preserved under Trans applied to
(Pos
V
,Neg
V
) for an assignment V .
Proof. For a consistent pair (Pos
V
,Neg
V
), let
(Pos
V
0
,Neg
V
0
)
be Trans(Pos
V
,Neg
V
), and examine any q ∈ Σ. With
Definition 2, the case for q to be included in Pos
V
0
(case (a)) and the cases for q to be included in Neg
V
0
(cases (b), (c) and (d)) are exclusive. Thus V
0
is well
defined such that (Pos
V
0
,Neg
V
0
) is consistent.
Fixed Point Semantics:
A partial order ⊆
com
on 2
Σ
× 2
Σ
is defined:
(Pos
V
,Neg
V
) ⊆
com
(Pos
V
0
,Neg
V
0
)
iff Pos
V
⊆ Pos
V
0
and Neg
V
⊆ Neg
V
0
The mapping Trans is not monotonic in the sense
that even if (Pos
V
1
,Neg
V
1
) ⊆
com
(Pos
V
2
,Neg
V
2
), it
does not mean that
Trans(Pos
V
1
,Neg
V
1
) ⊆
com
Trans(Pos
V
2
,Neg
V
2
).
Proposition 4. Assume a fixed point of Trans for an
assignment V to the set of rules Rule,
(Pos
V
,Neg
V
) = Trans(Pos
V
,Neg
V
).
Then eval
V
(Rule) = 1.
Proof. For each q ∈ Σ
Rule
, we check the evaluation of
the set Rule.
(a) If q ∈ Pos
V
, then
∀rule : [E f (rule) = q → eval
V
(rule) = 1].
(b) Let q ∈ Neg
V
. If there is no rule with E f (rule) =
q and no rule with E f (rule) = not q, do not care
this case for the evaluation of Rule.
(c) With q ∈ Neg
V
, and for any rule:
[eval
V
(Con(rule)) = 0 and eval
V
(E f (rule)) = 0],
eval
V
(rule) = 1.
(d) With q ∈ Neg
V
, we see that for any rule :
E f (rule) = not q, eval
V
(not q) = 1. Thus
eval
V
(rule) = 1.
(e) Assume q 6∈ Pos
V
∪ Neg
V
. For any rule:
E f (rule) = q, eval
V
(Con(rule)) = 0 or 1/2
and eval
V
(E f (rule)) = 1/2. It follows that
eval
V
(rule) = 1. For and rule : E f (rule) = not q,
eval
V
(Con(rule)) = 0 and eval
V
(E f (rule)) = 0.
Thus eval
V
(rule) = 1.
Logical Database:
By Proposition 4 for Rule, a fixed point of Trans,
(Pos
V
f ix
,Neg
V
f ix
), can be a model of Rule, with an as-
signment V
f ix
. The set Pos
V
f ix
contains predicates to
be retrieved, where the set Neg
V
f ix
contains predicates
to be negated by being not retrieved. Not all retrieval
predicates may be obtained from any Rule, however,
if a fixed point exists, retrievals are available in log-
ical database represented by BNF, even with strong
negation. Thus the BNF can be regarded as a design
to represent analysis of effectiveness.
The model pair
(Pos
V
f ix
,Neg
V
f ix
)
corresponds to the retrieval scheme for the set Rule as
database:
In the sense that
q ∈ Pos
V
f ix
⇒ q is retrieved,
q ∈ Neg
V
f ix
⇒ q is not retrieved, and
q 6∈ Pos
V
f ix
∪ Neg
V
f ix
⇒ retrieval of q is undefined,
the scheme is implemented. That is, for each query q
to database expressed by BNF, retrieval result is ex-
pected to answer
(i) Yes (if q ∈ Pos
V
f ix
),
(ii) No (if q ∈ Neg
V
f ix
) and
(iii) Unknown (otherwise).
Query q (predicate) −→ Recursive BNF
Rule
Yes/No/Unknown ←− (as Database)
4.3 Negation as Failure
To relax complexity caused by nonmonotonic map-
ping Trans, we focus on strong negation of the form
not q, to take the approximation that default or nega-
tion as failure may be substituted for strong negation.
The negation as failure is classically established:
If some predicate p cannot be derived from the set of
formulas Γ in a proof system, then p may be negated:
Γ 6` p ⇒ ¬p.
Approximate Evaluation on the Restricted Rule:
approx
V
is defined recursively, with respect to an
assignment V for Rule, where each rule of Rule con-
tains only the positive of the form q as E f (rule), that
is, each rule rule does not contain negation sign in
E f (rule).
COMPLEXIS 2022 - 7th International Conference on Complexity, Future Information Systems and Risk
62
approx
V
(Rule) =
[∀rule ∈ Rule : approx
V
(rule) = 1 → 1,
∃rule ∈ Rule : approx
V
(rule) = 0 → 0, 1/2]
approx
V
(rule) =
[approx
V
(Con) v approx
V
(E f ) → 1,
approx
V
(E f ) = 0 → 0, 1/2]
approx
V
(Con) =
[∀q ∈ Re : V (q) = 1 and
∀not q ∈ Pro : V (q) = 0 → 1,
∃q ∈ Pro : V (q) = 0 or
∃not q ∈ Pro : V (q) = 1 → 0, 1/2]
approx
V
(E f ) = V (q) for E f = q
approx
V
(not q) =
[V (q) = 0 → 1,V (q) = 1 → 0, 1/2]
We thus substitute negation as failure for strong
negation, in evaluation of Rule.
An evaluation function approx
V
is then analyzed
in the following.
Definition 5. A mapping
Tr : 2
Σ
× 2
Σ
→ 2
Σ
× 2
Σ
is defined, such that, with Tr to be applied to
(suc
V
, f ail
V
), (suc
V
0
, f ail
V
0
) may be obtained:
(a) If there exists a rule such that Con(rule) = null
Con
or approx
V
(Con(rule)) = 1, E f (rule) is in suc
V
0
.
(b) For any rule : approx
V
(Con(rule)) = 0, E f (rule)
is in f ail
V
0
.
Proposition 6. Assume the mapping
Tr : (2
Σ
× 2
Σ
) → (2
Σ
× 2
Σ
).
Consistency is preserved under Tr applied to
(suc
V
, f ail
V
) for an assignment V .
Proof. Let (suc
V
0
, f ail
V
0
) = Tr(suc
V
, f ail
V
). If
(suc
V
, f ail
V
) is consistent, the cases for E f (rule) to
be included in suc
V
0
and to be included in f ail
V
0
are
mutually exclusive. Therefore the pair (suc
V
0
, f ail
V
0
)
is consistent, so that consistency may be preserved
under the mapping Tr.
As regards comparison of the evaluation eval
V
with approx
V
, we have:
Proposition 7. For any “rule” of “Rule”,
eval
V
(Con(rule)) v approx
V
(Con(rule)),
and eval
V
(E f (rule)) = approx
V
(E f (rule)).
Proof. It is because eval
V
(not q) v approx
V
(not q),
for Con(rule), where
eval
V
(E f (rule)) = approx
V
(E f (rule))
for E f (rule) containing no negation sign.
For simplicity of treatment of the mapping Tr, let
T R : Ω → Ω be defined for the set
Ω = {V | V : Σ → {0,1/2,1} is an assignment }
with respect to Σ = Σ
Rule
such that
T R(V
1
) = V
2
iff
Tr(suc
V
1
, f ail
V
1
) = (suc
V
2
, f ail
V
2
).
Definition 8. A partial order v
assign
on the set Ω of
assignments is defined: V v
assign
V
0
if, for two pairs
(suc
V
, f ail
V
) and (suc
V
0
, f ail
V
0
),
(suc
V
, f ail
V
) ⊆
com
(suc
V
0
, f ail
V
0
).
The mapping T R is monotonic in the following
sense.
Proposition 9. If V
1
v
assign
V
2
, then
T R(V
1
) v
assign
T R(V
2
).
Proof. With the correspondence of the mapping
T R to Tr, we need that if (suc
V
1
, f ail
V
1
) ⊆
com
(suc
V
2
, f ail
V
2
), then
Tr(suc
V
1
, f ail
V
1
) ⊆
com
Tr(suc
V
2
, f ail
V
2
).
By the definition of approx
V
, we can see this.
Because the mapping T R is monotonic, there is a
(least) fixed point of T R.
Proposition 10. There is a fixed point V
0
of T R such
that T R(V
0
) = V
0
.
Proof. Following the ordinary monotonic function
theory on the complete lattice, we see that
u{V ∈ Ω | T R(V ) v
assign
V }
is a (least) fixed point of T R, where u stands for the
greatest lower bound.
With such a fixed point assignment V
0
, we have:
Proposition 11. For the restricted Rule and with a
fixed point V
0
of T R,
approx
V
0
(Rule) = 1 and eval
V
0
(Rule) = 1.
Proof. It is known that V
0
= T R
α
(
/
0
Ω
) for some or-
dinal α, where T R
β
(
/
0
Ω
) = T R(T R
β−1
(
/
0
Ω
)) for β:
successor ordinal, or t
γ<β
T R
γ
(
/
0
Ω
) for β: limit order
(with the least upper bound notation t), where:
(i)
/
0
Ω
∈ Ω denotes (
/
0,
/
0) ∈ 2
Σ
× 2
Σ
.
(ii) T R preserves consistency, and T R is inclusive
such that T R
α
preserves consistency.
It is seen that approx
/
0
Ω
(rule) = 1. In addition, for
any rule,
approx
/
0
Ω
(rule) v approx
T R
β
(
/
0
Ω
)
(rule),
with assignments
/
0
Ω
v
assign
T R
β
(
/
0
Ω
).
Thus approx
V
0
(rule) = 1 for any rule such that
approx
V
0
(Rule) = 1. With Proposition 7, for any
rule,
Consultation to Effectiveness and Logical Meaning
63
eval
V
0
(Con(rule)) v approx
V
0
(E f (rule))
= eval
V
0
(E f (rule)).
It follows that eval
V
0
(rule) = 1 for any rule, and thus
eval
V
0
(Rule) = 1.
5 CONCLUSION
This paper deals with abstraction of a teacher’s analy-
sis and synthesis such that the role of a consultant may
be described. If causal relation is analyzed by a con-
sultant to design a system, the abstract consultation
may be understood as a transformation of effective-
ness caused by analysis to design of representation
for database.
The primary result of this paper is to formulate
the role of a consultant as abstract consultation which
can be described in modal logic with the greatest fixed
point operator, even on the propositional base.
(i) The modal logic of this paper involves prefix
modality for analysis and postfix modality for design,
where both analysis and design are called by names.
(ii) Conditioning the behaviors to receive analysis
by prefix modality and to provide design by postfix
modality, we have formulas in our modal logic. The
denotation of a formula is presented by a state set,
where states virtually keep computing environments,
and state transitions are meaningful as relations re-
garding modal operators.
(iii) With respect to an equilibrium, a state set is given
as a greatest fixed point of the denotation for a for-
mula conditioned to the behavior of consultation.
As the secondary result, we have a model theory
in 3-valued domain for the representations by Backus-
Naur Form as designed database (corresponding to
given effects as causal relations).
(i) Different from those in problem solving by answer
set programming, model theory in 3-valued logic con-
ceives some hard problem. We defined a fixed point
semantics by some mapping associated with a given
BNF representation. It is a basis of retrieval in the
database to be represented by Backus-Naur Form.
(ii) It is not always the case that we could see a model
of any representation of database. In such model the-
ory, an approximate idea of strong negation by nega-
tion as failure is provided. In the case of negation
as failure (default) instead of strong negation, model
theory is easier for some restricted class of representa-
tions as database. The case with communication facil-
ities (Yamasaki and Sasakura, 2021b) is theoretically
relevant to the present case.
REFERENCES
Cardelli, L. and Gordon, A. (2000). Mobile ambients. The-
oret.Comput.Sci., 240(1):177–213.
Dam, M. and Gurov, D. (2002). Mu-calculus with ex-
plicit points and approximations. J.Log.Comput.,
12(1):119–136.
Droste, M., Kuich, W., and Vogler, H. (2009). Handbook of
Weighted Automata. Springer.
Fitting, M. (2002). Modal logics between propositional and
first-order. J.Log.comput., 12(6):1017–1026.
Gebser, M. and Schaub, T. (2016). Modeling and language
extensions. AI Magazine, 3(3):33–44.
Giordano, L., Martelli, A., and Schwind, C. (2000).
Ramification and causality in a modal action logic.
J.Log.Comput., 10(5):625–662.
Goldblatt, R. and Hodkinson, I. (2020). Strong com-
pleteness of modal logics over 0-dimensional metric
spaces. Rev.Log.Comput., 13(3):611–632.
Hanks, S. and McDermott, D. (1987). Nonmonotonic logic
and temporal projection. Artifi.Intelli., 33(3):379–
412.
Kaufmann, B., Leone, N., Perri, S., and Schaub, T. (2016).
Grounding and solving in answer set programming. AI
Magazine, 3(3):25–32.
Kooi, B. (2016). The ambiguity of knowability. Re-
view.Symb.Log., 9(3):421–428.
Kozen, D. (1983). Results on the propositional mu-calculus.
Theoret.Comput.Sci., 27(3):333–354.
Merro, M. and Nardelli, F. (2005). Behavioural theory for
mobile ambients. J.ACM., 52(6):961–1023.
Naumov, P. and Tao, J. (2019). Everyone knows that
some knows: Quantifiers over epistemic agents. Re-
view.Symb.Log., 12(2):255–270.
Rasga, J., Sernadas, C., and Carnielli, W. (2021). Reduction
techniques for proving decidability in logics and their
meet-combination. Bull.Symb.Log., 27(1):39–66.
Spalazzi, L. and Traverso, P. (2000). A dynamic logic
for acting, sensing and planning. J.Log.Comput.,
10(6):787–821.
Tennant, N. (2021). What is a rule of inference.
Rev.Symb.Log., 14(2):307–346.
Venema, Y. (2008). Lectures on the Modal Mu-Calculus.
ILLC, Amsterdam.
Yamasaki, S. and Sasakura, M. (2020). Modal mu-calculus
extension with description of autonomy and its alge-
braic structure. In Proceedings of the 5th International
Conference on Complexity, Future Information Sys-
tems and Risk, pages pages 63–71.
Yamasaki, S. and Sasakura, M. (2021a). Algebraic expres-
sions with state constraints for causal relations and
data semantics. In CCIS 1446, Data Management
Technologies and Applications, pages 245–266.
Yamasaki, S. and Sasakura, M. (2021b). Distributed strate-
gies and managements based on state constraint logic
with predicate for communication. In Proceedings of
the 6th International Conference on Complexity, Fu-
ture Information Systems and Risk, pages 78–85.
COMPLEXIS 2022 - 7th International Conference on Complexity, Future Information Systems and Risk
64
