**Computability
Logic**

(CoL)

Section 8**
**

**CoL-based knowledgebase and resourcebase
systems**

The
reason for
the failure of *x*(*p*(*x*) *p*(*x*)) as a
computability-theoretic principle is that the problem represented by
this
formula may have no effective solution --- that is, the predicate *p*(*x*)
may be undecidable. The reason why this principle would fail in the
context of
knowledgebase systems, however, is much simpler. A knowledgebase system
may
fail to solve the problem *x*(*Married*(*x*) *Married*(*x*)) not because
the
latter has no effective solution (of course it has one), but because
the system
simply lacks sufficient knowledge to tell any given person’s marital
status. On the
other hand, any system
would be able to “solve” the problem *x*(*Married*(*x*) *Married*(*x*)) as this is an
automatically won elementary game so that there is nothing to solve at
all.
Similarly, while *y**xFather*(*x*,*y*)
is an automatically solved elementary problem expressing the trivial
knowledge
that every person has a father, ability to solve the problem *y**xFather*(*x*,*y*)
implies the nontrivial knowledge of everyone’s actual father. Obviously
the
knowledge expressed by *A**B* or *xA*(*x*)
is generally stronger than the
knowledge expressed by *A**B* or *xA*(*x*),
yet the formalism of classical logic
fails to capture this difference --- the difference whose relevance
hardly
requires any explanation. The traditional approaches to knowledgebase
systems
try to mend this gap by augmenting the language of classical logic with
special
epistemic constructs, such as the modal “know that” operator □, after which
probably
□*A*□*B* would be
suggested as a translation for *A**B* and *y**x*□*A*(*x*,*y*)
for *y**xA*(*x*,*y*).
Leaving it for the philosophers to argue whether, say, *y**x*□*A*(*x*,*y*) really
expresses the constructive meaning of *y**xA*(*x*,*y*),
and forgetting that epistemic constructs often yield unnecessary and
unpleasant complications
such as
messiness and non-semidecidability of the resulting logics, some of the
major
issues still do not seem to be taken care of. Most of the actual
knowledgebase
and information systems are interactive, and what we really need is a
logic of *interaction* rather than
just a logic of
knowledge. Furthermore, a knowledgebase logic needs to be *resource-conscious*.
The informational
resource expressed by *x*(*Pregnant*(*x*) *Pregnant*(*x*)) is
not as strong as the
one expressed by *x*(*Pregnant*(*x*) *Pregnant*(*x*)) *x*(*Pregnant*(*x*) *Pregnant*(*x*)): the former
implies
the resource provider’s commitment to tell only one (even though an
arbitrary
one) woman’s pregnancy status, while
the
latter is about doing the same for any two Women.
The former is the informational resource
provided by a single disposable pregnancy test device, while the latter
is the
resource provided by two such devices. Neither classical logic nor its
standard
epistemic extensions have the ability to account for such differences.
But CoL
promises to be adequate. It *is* a
logic of interaction, it *is*
resource-conscious, and it *does*
capture the relevant differences between truth and actual ability to
find/compute/know truth.

When
CoL is
used as a logic of knowledgebases, its
formulas represent interactive queries. A formula whose main operator
is or
can
be understood as a
question asked by the
user, and a formula whose main operator is or
as
a question asked by the
system. Consider
the problem *x**yHas*(*x*,*y*),
where *Has*(*x*,*y*) means
“patient *x*
has disease *y*”
(with *Healthy* counting as one of
the
possible “diseases”). This formula is the following question asked by
the
system: “Who do you want me to diagnose?”
The user's response can be “Laura”. This move brings the
game down to *yHas*(*Laura*,*y*). This is now a question asked by the
user: “What does Laura
have?”. The system’s response can be “flu”, taking us to the terminal
position *Has*(*Laura*,*Flu*).
The system has been successful iff
Laura really has the flu.

Successfully
solving the above problem *x**yHas*(*x*,*y*) requires
having all relevant medical
information for each possible patient, which in a real diagnostic
system would
hardly be the case. Most likely, such a system, after receiving a
request to
diagnose *x*, would make
counterqueries
regarding *x*’s symptoms, blood
pressure, test results, age, gender, etc., so that the query that the
system
will be solving would have a higher degree of interactivity than the
two-step
query *x**yHas*(*x*,*y*)
does, with questions and counterquestions interspersed in some complex
fashion.
Here is when other CoL operations come into play. Negation
turns
queries into counterqueries; parallel operations
generate combined queries; recurrence operations allow repeated
queries; implications
and rimplications act as various sorts of query reduction operations;
etc. Here
we are expanding our example. Let *Sympt*(*x*,*s*)
mean “patient *x* has (set of)
symptoms
*s*”, and *Pos*(*x*,*t*)
mean “patient *x* tests positive for
test *t*”.
Imagine a diagnostic system which can diagnose any particular patient *x*, but needs some additional
information. Specifically, it needs to know *x*’s
symptoms; plus, the system may require to have *x*
taken a test *t* which it
selects dynamically in the course of a dialogue with the user depending
on what
responses it received. The interactive task/query that such a system is
performing/solving can then be expressed by the following formula,
which we
shall call *Diagn* for further
references:

*Diagn* ≡ *x*(*s*Sympt(*x*,*s*) *t*(*Pos*(*x*,*t*) *Pos*(*x*,*t*)) *yHas*(*x*,*y*)).

A
possible
scenario of playing the above game is the
following. At the beginning, the system waits until the user specifies
a
patient *x* to be diagnosed. We can
think of this stage as systems’s requesting the user to select a
particular
(value of) *x*, remembering that the
presence of *x* automatically
implies such a request. After a patient *x*
--- say *x*=*X*
--- is selected, the system requests to specify *X*’s
symptoms. Notice that our game rules
make the system successful if the user fails to provide this
information, i.e.
specify a (the true) value for *s* in
*sSympt*(*X*,*s*).
Once a response --- say, *s*=*S* --- is
received, the system selects a
test *t*=*T*
and asks the user to perform it on *X*,
i.e. to choose the true disjunct of
*Pos*(*X*,*T*) *Pos*(*X*,*T*).
Finally,
provided that the user gave correct answers
to all counterqueries (and if not, the user has lost), the system makes
a
diagnostic decision, i.e. specifies a value *Y*
for *y* in *yHas*(*X*,*y*)
for which *Has*(*X*,*Y*) is
true.

The
presence
of a single “copy” of *t*(*Pos*(*x*,*t*) *Pos*(*x*,*t*)) in the
antecedent
of *Diagn
*means
that the system may request testing a given patient only once. If up to
*n* tests were potentially needed
instead,
this would be expressed by taking the -conjunction
of *n* identical conjuncts *t*(*Pos*(*x*,*t*) *Pos*(*x*,*t*)). And if the
system
potentially needed an unbounded number of tests, then we would write *t*(*Pos*(*x*,*t*) *Pos*(*x*,*t*)), thus further
weakening *Diagnoser*: a system that
performs this weakened task
is
not as good as the one performing the original *Diagn*, as it
requires stronger external (user-provided) informational resources.
Replacing
the main quantifier *x* by *x*, on the other
hand,
would strengthen *Diagn*,
signifying the system’s ability to diagnose a patent purely on the
basis of
his/her symptoms and test result without knowing who the patient really
is.
However, if in its diagnostic decisions the system uses some additional
information on patients such their medical histories stored in its
knowledgebase and hence needs to know the patient’s identity, *x* cannot be
upgraded
to *x*. Replacing *x* by *x* would be a
yet
another way to strengthen *Diagn*,
signifying the system’s ability to diagnose all patients rather than
any
particular one; obviously effects of at least the same strength would
be
achieved by just prefixing *Diagn*
with or
.

** knowledgebase**,
let us
make clear what it means. Formally, this is a finite -conjunction

The
knowledgebase *KB*
of the system may include atomic elementary formulas expressing factual
knowledge, such as *Married*(*Laura*), or
non-atomic elementary
formulas expressing general knowledge, such as *x*(*yFather*(*x*,*y*) *M ale*(*x*)) and *x**y*(*x*✕(*y*+1) = (*x*✕*y*)+*x*); it can also
include nonclassical formulas such as *x*(*Female*(*x*) * Male*(*x*)), expressing
potential knowledge of everyone's gender, or *x**y*(*x*^{2}=*y*), expressing ability to repeatedly
compute the square
function, or something more complex and more interactive, such as the
earlier
seen formula *Diagn*.
With each resource *R*?#381;*KB* is associated
(if not physically, at least
conceptually) its ** provider**
--- an agent that solves the query

The
most
typical internal informational resources,
such as factual knowledge or queries solved by computer programs, can
be reused
an arbitrary number of times and with unlimited branching capabilities,
i.e. in
the strong sense captured by , and thus
they
would be prefixed with a

Assume
*KB* = *R*_{1}_{} ... *R _{n}*, and let us
now try
to visualize a system solving a query

*F*
reduces to its ability to generate a
solution for *KB**F*, i.e.
generate a
reduction of *F* to *KB*.
What would give the system such an
ability is built-in knowledge of CoL --- in particular, a ** uniform-constructively
sound axiomatization** of it. According to
the uniform-constructive
soundness property, it would be sufficient for the system to find a
proof of

Notice that it is uniform-constructive
soundness rather
than simple soundness of the built-in (axiomatization of the) logic
that allows
the knowledgebase system to function. By *simple
soundness* here we mean that every provable formula is
nonlogically valid.
This is not sufficient for two reasons.

*E*
only implies that, for every
interpretation *, a solution for the problem *E**
exists. It may be the case, however, that
different interpretations require different
solutions, so that choosing the right solution requires knowledge of
the actual
interpretation, i.e. the *meaning*,
of
the atoms of *E*. Our assumption is
that the system has no nonlogical knowledge, which, in more precise
terms,
means nothing but that
it has no
knowledge of the interpretation *. Thus, a solution that the system
generates
for *E** should be successful for any
possible interpretation *. In other words, it should be a uniform
solution for *E*. This is where
uniform-constructive
soundness of the underlying logic becomes critical, by which every
provable
formula is not only nonlogically, but also logically
valid.

The
other
reason why simple soundness of the built-in
logic would not be sufficient for a knowledgebase system to function
--- even
if every provable formula was known to be logically valid --- is the
following.
With simple soundness, after finding a proof of *E*,
even though the system would know that a solution for *E**
exists, it might have no way to
actually find such a solution. On the other hand, uniform-constructive
soundness guarantees that a (uniform) solution for every provable
formula not
only exists, but can be effectively extracted from a proof.

As
for
completeness of the built-in logic, unlike
uniform-constructive soundness, it is a desirable but not necessary
condition.
So far complete axiomatizations have been found only for various
limited
fragments of the language of CoL. We hope that the future will bring
completeness results for more and more expressive fragments as well.
But even
if not, we can still certainly succeed in finding ever stronger
axiomatizations
that are uniform-constructively sound even if not necessarily complete.
It
should be remembered that, when it comes to practical applications in
the
proper sense, the logic that will be used is likely to be far from
complete
anyway. For example, the popular classical-logic-based systems and
programming
languages are incomplete, and the reason is not that a complete
axiomatization
for classical logic is not known, but rather the unfortunate fact of
life that
often efficiency only comes at the expense of completeness.

**CL4**,
despite the absence of recurrence operators
in it, is already very powerful. Why don’t we see a simple example to
get the
taste of it as a query-solving logic. Let, as before, *Acid*(*x*) mean “solution *x*
contains acid”, and *Red*(*x*)
mean “litmus paper turns red in solution *x*”.
Assume that the knowledgebase *KB* of
a
**CL4**-based system contains *x*(*Red*(*x*) ↔* Acid*(*x*)) and *x*(*Red*(*x*) *Red*(*x*)), accounting
for
knowledge of the fact that a solution contains acid iff the litmus
paper turns
red in it, and for availability
of a
provider who possesses a piece of litmus paper that it can dip into any
solution and report the paper’s color to the system. Then the system
can solve
the acidity query *x*(*Acid*(*x*) *Acid*(*x*)). This follows
from
the fact, left as an exercise for the reader to verify, that **CL4** proves *KB * *x*(*Acid*(*x*) *Acid*(*x*)).

The
context of
knowledgebase systems can be further
extended to systems for planning and action. Roughly, the formal
semantics in
such applications remains the same, and what changes is only the
underlying
philosophical assumption that the truth values of predicates and
propositions
are fixed or predetermined. Rather, those values in CoL-based planning
systems will be viewed as something that interacting agents may be able
to manage.
That is,
predicates or propositions there stand for *tasks*
rather than *facts*. E.g., *Pregnant*(*Laura*)
--- or, perhaps, *Impregnate*(*Laura*)
instead --- can be seen as having
no predetermined truth value, with Laura or her mate being in control
of
whether to make it true or not. And the nonelementary formula *xHit*(*x*)
describes the task of hitting any one
target *x* selected by the
environment/commander/user. Note how naturally resource-consciousness
arises
here: while *xHit*(*x*)
is a task accomplishable with one
ballistic missile, the stronger task *xHit*(*x*) *xHit*(*x*)
would require two missiles instead.
All of the other operators of CoL, too, have natural interpretations as
operations on physical (as opposed to just informational) tasks, with acting
as a task reduction
operation. To get a
feel of this, let us look at the task

*Give me a
wooden stake* *Give
me
a silver bullet* *Destroy
the vampire* *Kill
the
werewolf*.

This
is a task
accomplishable by an agent who has a
mallet and a gun as well as sufficient time, energy and bravery to chase and eliminate any
one (but not both)
of the two monsters, and only needs
a
wooden stake and/or a silver bullet to complete his noble mission. Then
the
story told by the legal run 〈1.1, 0.1〉 of the above
game is that the environment asked the
agent to kill the werewolf, to which the agent replied by the
counterrequest to
give him a silver bullet. The task will be considered eventually
accomplished
by the agent iff he indeed killed the werewolf as long as a silver
bullet was
indeed given to him.