Algorithm-Supported Mathematical Theory Exploration: A Personal View and Strategy - Artificial Intelligence and Symbolic Computation - page 243

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 ]