Information Technology Reference
In-Depth Information
val EfnDef
=
def
(
Efn
(
World,w0,Ifn,Jfn)
(
pv s)
=
Ifn World
(
pv s) INTER World) ∧
(
Efn
(
World,w0,Ifn,Jfn)
(
nots s1)
=
World DIFF Efn
(
World,w0,Ifn,Jfn) s1) ∧
(
Efn
(
World,w0,Ifn,Jfn)
(
s1 ands s2)
=
Efn
(
World,w0,Ifn,Jfn) s1 INTER Efn
(
World,w0,Ifn,Jfn) s2) ∧
(
Efn
(
World,w0,Ifn,Jfn)
(
s1 ors s2)
=
Efn
(
World,w0,Ifn,Jfn) s1 UNION Efn
(
World,w0,Ifn,Jfn) s2) ∧
(
Efn
(
World,w0,Ifn,Jfn)
(
s1 imps s2)
=
World DIFF Efn
(
World,w0,Ifn,Jfn) s1 UNION
Efn
(
World,w0,Ifn,Jfn) s2) ∧
(
Efn
(
World,w0,Ifn,Jfn)
(
s1 eqs s2)
=
(
World DIFF Efn
(
World,w0,Ifn,Jfn) s1 UNION
Efn
(
World,w0,Ifn,Jfn) s2) INTER
(
World DIFF Efn
(
World,w0,Ifn,Jfn) s2 UNION
Efn
(
World,w0,Ifn,Jfn) s1)) ∧
(
Efn
(
World,w0,Ifn,Jfn)
(
P says s1)
=
{ w14 | Rfn
(
World,w0,Ifn,Jfn) P Rwith w14 SUBSET
Efn
(
World,w0,Ifn,Jfn) s1}) ∧
(
Efn
(
World,w0,Ifn,Jfn)
(
P speaks for Q)
=
{
y
|
Rfn
(
World,w0,Ifn,Jfn) Q SUBSET Rfn
(
World,w0,Ifn,Jfn) P
∧
y IN World})
(
Efn
(
World,w0,Ifn,Jfn)
(
P eqp Q)
=
{y |
(
Jext
(
World,w0,Ifn,Jfn) P
=
Jext
(
World,w0,Ifn,Jfn) Q) ∧
y IN World}) : thm
We can then formally define the models predicate (
|
=) as follows:
val ModelFnDef
=
def
∀World w0 Ifn Jfn w1 s.
((
World,w0,Ifn,Jfn),w1) MD s
=
w1 IN World ⊃
w1 IN Efn
(
World,w0,Ifn,Jfn)s:thm
Using the models predicate, we proved the soundness of the axioms intro-
duced in [5]. Specifically we proved as sound the standard modal properties
(S2-S4). We did not directly prove sound S1, which corresponds to the first rule
in Figure 1:
if
ϕ
is an instance of a propositional-logic tautology
ϕ
To prove this in HOL would require proving each tautology separately. Instead,
we proved only those tautologies that we needed for our specific examples.
We also proved as sound the axioms relating the modal logic to the calculus
of principals (i.e., the axioms P1, P2, P3, P5, P6, P7). However, we did not prove
soundness of their hand-off axiom (P10), because (as noted in their paper) it is
not sound. Appendix A provides a partial list of axioms and theorems we have
proved sound.
