There are several examples of active logics in our papers. We present
here a couple of simple ones.
t: Now(t)
----------
t+1: Now(t+1)
is a rule that says: if at the current step, Now has the value t,
then, at the next step, let Now have the value (t + 1). This enables
the active logic to keep track of step numbers and therefore of time.
This is a basic rule and is included in all active logics.
Another example is the contradiction rule:
t: P, not(P)
-----------------
t+1: contra(P, not(P))
If at a step, we have both P and not(P) present in the database, at
the next step, we add contra(P, not(P)) to the database to indicate
the contradiction. There will be other rules that will cause the
consequences of P and not(P) not to be derived in later steps, and
rules that will attempt to resolve the contradiction and reinstate
either P or not(P) to the database at a later time.
We can also have modus ponens:
t: P, P -> Q
--------------
t+1: Q
This says: if at time t, the database contains P and (P -> Q), then in
the next time step, conclude Q.
Note that if the database contains P, (P -> Q) and (Q -> R), we do not
get R immediately, but only after 2 steps. First, we use P and (P ->
Q) to obtain Q, then in the second step, we use this together with (Q
-> R) to derive R.
The inheritance rule keeps formulas in the database unless there is a
contradiction:
t: P , not_know(not(P)), \+ P = Now(t)
-------------------------------------
t + 1: P
t: P , not_know(P)
------------------------
t + 1: not(P)
not_know(P) is true iff P is not in the current database. Since the
database is finite, this poses no computational problems. "\+ P =
Now(t)" verifies that P is not of the form Now(t) and prevents time
form being inherited.
This pair of rules causes contradictions not to be present after they
are detected.
Let the sentences initially present in the database be: Now(0),
Bird(tweety), Bird(x) & not_know(not(fly(x))) -> fly(x). With the
above rules of inference, this is what the database looks like at
consecutive steps:
At step 0:
Now(0), Bird(tweety), Bird(x) & not_know(not(fly(x))) -> fly(x)
At step 1:
Now(1), Bird(tweety), Bird(x) & not_know(not(fly(x))) -> fly(x),
fly(tweety)
since "not(fly(tweety))" is not present in the database at step 0.
The database will not change thereafter.
Now assume that the initial set of sentences is: Now(0),
Bird(tweety), Bird(x) & not_know(not(fly(x))) -> fly(x),
not(fly(tweety)).
This time we get:
At step 0:
Now(0), Bird(tweety), Bird(x) & not_know(not(fly(x))) -> fly(x),
not(fly(tweety))
At step 1:
Now(1), Bird(tweety), Bird(x) & not_know(not(fly(x))) -> fly(x),
not(fly(tweety))
This time, we cannot conclude that tweety flies since we know he
doesn't, i.e., not_know(not(fly(tweety))) fails since not(fly(tweety))
is present at step 0.
|
