Information Technology Reference

In-Depth Information

Q
[
x, y
]

.

P
[
x, y
]

P
[
y, x
]

∀
x,y

⇔

Invention of a new proposition:

If we assume that we are working w.r.t. a knowledge base
K
in which two

binary predicate constants
P
and
Q
occur, then we may apply the above scheme

by conjecturing

AR
[
Q, P
]
,

i.e.

Q
[
x, y
]

.

P
[
x, y
]

P
[
y, x
]

⇔

We may now use a suitable (automated) prover from our prover library and

try to prove or disprove this formula. In case the formula can be proved, we may

say that the application of the above scheme “invented a new proposition on the

known notions
P
and
Q
”.

Invention of a problem:

Given a binary predicate constant
P
in the knowledge base
K
,wemayask

to “find” a
Q
such that

AR
[
Q, P
]
.

In this case, application of the scheme
AR
“invents a problem”. The nature

of the problem specified by
AR
depends on what we allow as “solution”
Q
.

If we allow any binary predicate constant occurring in
K
then the problem is

basically a “method retrieval and verification” problem in
K
: We could consider

all or some of the binary predicate constants
Q
in
K
as candidates and try to

prove/disprove
AR
[
Q, P
]. However, typically, we will allow the introduction of a

new constant
Q
and ask for the invention of formulae
D
that “define”
Q
so that,

using
K
and
D
,
AR
[
Q, P
] can be proved. Depending on which class of formulae

we allow for “defining”
Q
(and possible auxiliary operations), the diculty of

“solving the problem” (i.e. finding
Q
) will vary drastically. In the simple example

above, if we allow to use the given
P
and explicit definitions, then the problem

is trivially solved by the formula
AR
[
Q, P
] itself, which can be considered as an

“algorithm” w.r.t. the auxiliary operation
P
. If, however, we allow only the use

of certain elementary algorithmic functions in
K
and only the use of recursive

definitions then this problem may become arbitrarily dicult.

Invention of a method (algorithm):

This case is formally identical to the case of invention of an axiom or def-

inition. However methods are normally seen in the context of problems. For

example if we have a problem

PR
[
Q, R
]

of finding an operation
Q
satisfying
PR
in relation to certain given operations

R
then we may try the proposal

AR
[
Q, P
]

Search WWH ::

Custom Search