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

*To*: thkim@salmosa.kaist.ac.kr (Tae Ho Kim)*Subject*: Re: instantiation*From*: John Hoffman <hoffman@securecomputing.com>*Date*: Thu, 3 Jul 1997 11:30:18 -0500 (CDT)*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <199707031616.BAA08110@salmosa.kaist.ac.kr> from "Tae Ho Kim" at Jul 4, 97 01:16:09 am

your thoerem is not true. a3 < a4 AND a4 < a3 could be true or false and still be consistent with the set of axioms that you have defined. You might wish to define some more. You have assumed term is transitive, you might wish to add anti_symmetric, and/or reflexivity. These concepts are all defined in the prelude. John > > Hi. > > I would like to prove THEOREM test in theory s : > Could you help me? > > s: THEORY > BEGIN > > term: TYPE = { a1,a2,a3,a4,a5} > < : PRED[[term, term]] > trans : AXIOM FORALL (x,y,z:term): > x < y AND y < z IMPLIES x < z > > ax0 : AXIOM a1 < a2 > ax1 : AXIOM a2 < a4 > ax2 : AXIOM a3 < a5 > > test : THEOREM FORALL (a,b:term): NOT ((a<b) AND (b<a)) > > END s > > > ----- > thkim@salmosa.kaist.ac.kr > >

**References**:**instantiation***From:*Tae Ho Kim <thkim@salmosa.kaist.ac.kr>

- Prev by Date:
**instantiation** - Next by Date:
**Re: instantiation** - Prev by thread:
**instantiation** - Next by thread:
**Re: instantiation** - Index(es):