Temporal Logic
-------- -----

PF (Past/Future) Temporal Logic is like propositional
calculus, except that instead of a proposition p being
either TRUE or FALSE, p has a possibly different value
of TRUE or FALSE at each of several times t.  Thus a
proposition p is a function from times in some set T to
the 2-element set {TRUE, FALSE}.  Alternatively, we may
view p as a subset of T, namely the set of all times for
which p is TRUE.

There is an order relation < on times, but there are no
fixed rules about how this relation behaves.  That is,
given times t1 and t2, one would expect that one of
t1 < t2, or t1 = t2, or t1 > t2, but we do NOT require
this; several or none of these may be true.  We even
permit a time t to be in its own future, i.e., t < t,
which means its also in its own past.

Pp means that proposition p was true at some time in the
past.  Fp means that p will be true at some time in the
future.  p(t) is the value, TRUE or FALSE, of proposi-
tion p at time t.  Therefore

	(Pp)(t) = there exists an s < t such that p(s)

	(Fp)(t) = there exists an s > t such that p(s)

We define the logical expressions e of PF Temporal Logic
as

	e ::= p | q | r		[propositions]
	    | (~e)		[negation]
	    | (e&e)		[logical conjunction]
	    | (e|e)		[logical disjunction]
	    | (Pe)		[was true operation]
	    | (Fe)		[will be true operation]
	    | constant

The classical logical operators ~, &, and | are defined
`pointwise' for temporal logic:

	(~p)(t)  = ~(p(t))
	(p&q)(t) = (p(t)&q(t))
	(p|q)(t) = (p(t)|q(t))

For standard propositional logic the constants are TRUE
and FALSE.  But in temporal logic, constants are func-
tions mapping the set of times T to the values TRUE or
FALSE, and may be alternatively represented as the sub-
set of T on which the function takes the value TRUE.

For this problem we will take T to be the set of the
single digit numbers, 0, 1, 2, 3, 4, 5, 6, 7, 8, and 9.
We will write a subset of T by listing the digits in the
subset in parentheses.  Thus (345) denotes the set of
times {3, 4, 5}, and () denotes the empty set of times.
These are our logical constants.

With this notation we find that

    (~(23478)) = (01569)

    ((12345)&(456789)) = (45)

    ((123)|(345)) = (12345)

If in addition we assume that < is the standard order on
digits, then

    (P(35)) = (456789)

    (F(235)) = (01234)

In general, < will be an arbitrary relation which we
define with a 10x10 matrix of characters.  Each of the
10 rows corresponds to a row digit, R, going from 0 at
the top to 9 at the bottom.  Each of the 10 columns
corresponds to a column digit, C, going from 0 at the
left to 9 at the right.  The matrix position for R and
C is `X' if R<C is true and `.' if R<C is false.  Thus
if the matrix is given with one row per line, the matrix

	.XXXXXXXXX
	..XXXXXXXX
	...XXXXXXX
	....XXXXXX
	.....XXXXX
	......XXXX
	.......XXX
	........XX
	.........X
	..........

corresponds to the standard ordering of the digits.



Input
-----

For each of several test cases:

	one line containing the name of the test case
	10 lines each of 10 characters containing the
	   matrix representation of the < relation,
	   as described above
	any number of non-empty lines each containing
	    a logical expression
	an empty line (with no characters)

Input ends with an end of file.

There are no whitespace characters in any input line
except perhaps the test case name line.

The logical expressions either have no propositional
variables, or have `p' and/or `q' as their only proposi-
tional variables.


Output
------

For each test case:

	one line copying the name of the test case
	for each input logical expression, one line
	    beginning with an exact copy of the logical
	    expression and followed by one of:

	    	= <value of expression>
		is valid
		is satisfiable
		is unsatisfiable

	one empty line

If there is no proposition letter in the logical expres-
sion, output ` = <value of expression>' after the logi-
cal expression, where the value of the expression is a
constant with the form of zero or more digits in paren-
theses; i.e., `(357)'.  The digits in the parentheses
MUST BE IN ASCENDING ORDER.

If the logical expression contains propositions p or q,
then output ` is valid' after the logical expression if
the logical expression is TRUE at ALL times for ALL
values of p and q.  Such a formula is an axiom or
theorem of PF Temporal Logic for the given structure of
time (T,<).

Otherwise if the logical expression is TRUE at ALL times
for SOME p value and SOME q value, then output ` is
satisfiable' after the logical expression.

Otherwise output ` is unsatisfiable' after the logical
expression.  This means that for EVERY value of p and
EVERY value of q the expression is FALSE at SOME time.

For example, `((Fp)|(~(F(Fp))))' is an axiom that
is true for all times and values of p if and only if
< is a transitive relation on times.  So only for
transitive < is this formula `valid'.

The ONLY whitespaces in any output line are those
surrounding `=' and `is', and those copied in the
test case name line.  The last line output is empty.


Sample Input
------ -----

SAMPLE 1
.XXXXXXXXX
..XXXXXXXX
...XXXXXXX
....XXXXXX
.....XXXXX
......XXXX
.......XXX
........XX
.........X
..........
(~(23478))
((12345)&(456789))
((123)|(345))
(P(35))
(F(235))
((Fp)|(~(F(Fp))))
((~p)&p)
(p&q)

SAMPLE 2
.XXXXXXXX.
..XXXXXXXX
...XXXXXXX
....XXXXXX
.....XXXXX
......XXXX
.......XXX
........XX
.........X
..........
((Fp)|(~(F(Fp))))


[The last input line is an empty line.]


Sample Output
------ ------

SAMPLE 1
(~(23478)) = (01569)
((12345)&(456789)) = (45)
((123)|(345)) = (12345)
(P(35)) = (456789)
(F(235)) = (01234)
((Fp)|(~(F(Fp)))) is valid
((~p)&p) is unsatisfiable
(p&q) is satisfiable

SAMPLE 2
((Fp)|(~(F(Fp)))) is satisfiable


[The last output line is an empty line.]


File:	   temporal.txt
Author:	   Bob Walton <walton@deas.harvard.edu>
Date:	   Wed Oct 11 10:34:05 EDT 2006

The authors have placed this file in the public domain;
they make no warranty and accept no liability for this
file.

RCS Info (may not be true date or author):

    $Author: walton $
    $Date: 2006/10/11 14:35:04 $
    $RCSfile: temporal.txt,v $
    $Revision: 1.6 $