[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Help with PVS theorem proving



Hello,
I have been trying to prove one theorem for a PVS theory
that I have implemented for my research work. I have been trying all the
different strategies as discussed in the PVS theorem Prover but I have not
been able to prove them. I am sending in the theory in the
later part of this email.
I would appreciate if I could get comments on the implementation or the
proving strategies that I should do in order to make these theories work.
Thanking you, in anticipation.

Uma
*************************************************************************
Theory 1: File name
Objective: Proving a relationship by negation
*************************************************************************
checking  :THEORY
BEGIN

mybool:TYPE+={TRUE,FALSE}
P: mybool
M_C:mybool
M_T:mybool
P_E:mybool
V_V:mybool
T_V:mybool
W_S:mybool
B_V:mybool
E_T:mybool
Status:mybool

Rule:AXIOM ((P=FALSE)AND(M_C=TRUE)AND(M_T=TRUE)AND(P_E=TRUE) AND
(V_V=TRUE) AND (T_V=TRUE) AND (W_S=TRUE) AND (B_V=TRUE) AND (E_T=TRUE)) IMPLIES
(Status=FALSE)

Rule1:AXIOM ((P_E=FALSE) AND (M_C=TRUE) AND (M_T=TRUE) AND (P=TRUE) AND
(V_V=TRUE) AND (T_V=TRUE) AND (W_S=TRUE) AND (B_V=TRUE) AND (E_T=TRUE)) IMPLIES
(Status=FALSE)

Rule2: AXIOM ((M_C=FALSE) AND (P_E=TRUE) AND (M_T=TRUE) AND (P=TRUE) AND
(V_V=TRUE) AND (T_V=TRUE) AND (W_S=TRUE) AND (B_V=TRUE) AND (E_T=TRUE)) IMPLIES
(Status=FALSE)

 Rule3:AXIOM ((M_T=FALSE) AND (P_E=TRUE) AND (M_C=TRUE) AND (P=TRUE) AND
(V_V=TRUE) AND (T_V=TRUE) AND (W_S=TRUE) AND (B_V=TRUE) AND (E_T=TRUE)) IMPLIES
(Status=FALSE)

 Rule4: AXIOM ((V_V=FALSE) AND (P_E=TRUE) AND (M_C=TRUE) AND (P=TRUE) AND
(M_T=TRUE) AND (T_V=TRUE) AND (W_S=TRUE) AND (B_V=TRUE) AND (E_T=TRUE)) IMPLIES
(Status=FALSE)

 Rule5:AXIOM ((T_V=FALSE) AND (P_E=TRUE) AND (M_C=TRUE) AND (P=TRUE) AND
(M_T=TRUE) AND (V_V=TRUE) AND (W_S=TRUE) AND (B_V=TRUE) AND (E_T=TRUE)) IMPLIES
(Status=FALSE)

Rule6: AXIOM ((W_S=FALSE) AND (P_E=TRUE) AND (M_C=TRUE) AND (P=TRUE) AND
(M_T=TRUE) AND (T_V=TRUE) AND (V_V=TRUE) AND (B_V=TRUE) AND (E_T=TRUE))
IMPLIES(Status=FALSE)

 Rule7: AXIOM ((E_T=FALSE) AND (P_E=TRUE) AND (M_C=TRUE) AND (P=TRUE) AND
(M_T=TRUE) AND (T_V=TRUE) AND (W_S=TRUE) AND (B_V=TRUE) AND (V_V=TRUE)) IMPLIES
(Status=FALSE)

 Rule8: AXIOM ((B_V=FALSE) AND (P_E=TRUE) AND (M_C=TRUE) AND (P=TRUE) AND
(M_T=TRUE) AND (T_V=TRUE) AND (W_S=TRUE) AND (E_T=TRUE) AND (V_V=TRUE)) IMPLIES
(Status=FALSE)

FINAL: THEOREM (M_C=TRUE AND M_T=TRUE AND P=TRUE AND P_E=TRUE AND V_V=TRUE
AND T_V=TRUE AND W_S=TRUE AND B_V=TRUE AND E_T=TRUE) IMPLIES Status=TRUE

 END checking

*****************************************************************************