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

*To*: PVS Help <pvs-help@csl.sri.com>*Subject*: Re: [PVS-Help] Help with PVS theorem proving*From*: Jerry James <james@ittc.ku.edu>*Date*: Wed, 04 May 2005 10:24:12 -0500*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <Pine.GSO.4.58.0412180029320.28614@acadie.ece.concordia.ca>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com*User-Agent*: Gnus/5.1006 (Gnus v5.10.6) XEmacs/21.4 (Jumbo Shrimp, linux)

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/

**References**:**[PVS-Help] Help with PVS theorem proving***From:*Umabharathi Ramachandran <u_ramach@encs.concordia.ca>

- Prev by Date:
**[PVS-Help] Help with PVS theorem proving** - Next by Date:
**[PVS-Help] args1 and strategies** - Prev by thread:
**[PVS-Help] Help with PVS theorem proving** - Next by thread:
**[PVS-Help] Free Variables Not Allowed** - Index(es):