Re: [PVS-Help] Help with PVS theorem proving

[Jerry James <james@ittc.ku.edu>]

Umabharathi Ramachandran <u_ramach@encs.concordia.ca> wrote:
> 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.

On the implementation, why are you using your own boolean type?  Using
the prelude-defined boolean type would make things a lot clearer, in my
opinion:

checking: THEORY
 BEGIN

  P, M_C, M_T, P_E, V_V, T_V, W_S, B_V, E_T, Status: bool

  Rule: AXIOM
    NOT P AND M_C AND M_T AND P_E AND V_V AND T_V AND W_S AND B_V AND E_T
     IMPLIES NOT Status

  Rule1: AXIOM
    NOT P_E AND M_C AND M_T AND P AND V_V AND T_V AND W_S AND B_V AND E_T
     IMPLIES NOT Status

  Rule2: AXIOM
    NOT M_C AND P_E AND M_T AND P AND V_V AND T_V AND W_S AND B_V AND E_T
     IMPLIES NOT Status

  Rule3: AXIOM
    NOT M_T AND P_E AND M_C AND P AND V_V AND T_V AND W_S AND B_V AND E_T
     IMPLIES NOT Status

  Rule4: AXIOM
    NOT V_V AND P_E AND M_C AND P AND M_T AND T_V AND W_S AND B_V AND E_T
     IMPLIES NOT Status

  Rule5: AXIOM
    NOT T_V AND P_E AND M_C AND P AND M_T AND V_V AND W_S AND B_V AND E_T
     IMPLIES NOT Status

  Rule6: AXIOM
    NOT W_S AND P_E AND M_C AND P AND M_T AND T_V AND V_V AND B_V AND E_T
     IMPLIES NOT Status

  Rule7: AXIOM
    NOT E_T AND P_E AND M_C AND P AND M_T AND T_V AND W_S AND B_V AND V_V
     IMPLIES NOT Status

  Rule8: AXIOM
    NOT B_V AND P_E AND M_C AND P AND M_T AND T_V AND W_S AND E_T AND V_V
     IMPLIES NOT Status

  FINAL: THEOREM
    M_C AND M_T AND P AND P_E AND V_V AND T_V AND W_S AND B_V AND E_T
     IMPLIES Status

 END checking

As for the proof strategy, I'm afraid you have problems there.  The
theorem as stated is not true.  Your axioms give various situations in
which Status is required to be false, but never require Status to be
true.  Hence, it may be that Status is always false.
-- 
Jerry James
http://www.ittc.ku.edu/~james/