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

*To*: Tae Ho Kim <thkim@salmosa.kaist.ac.kr>*Subject*: Re: instantiation*From*: Natarajan Shankar <shankar@csl.sri.com>*Date*: Thu, 03 Jul 1997 09:41:17 -0700*cc*: pvs-help@csl.sri.com*In-reply-to*: Your message of "Fri, 04 Jul 1997 01:16:09 +0900." <199707031616.BAA08110@salmosa.kaist.ac.kr>

Kim: I'm unable to see why that should be a theorem. Your axioms provide no way of proving that a < b doesn't hold. ax0, ax1, ax2 assert a < b for some a's and b's, and trans allows a < b assertions to be chained. But there is no way of obtaining a NOT a < b assertion from these axioms. You perhaps know that the enumerated type generates an ord function so that ord(a1) = 0, ..., ord(a5) = 4. This can be used to define a < b as ord(a) < ord(b). With this definition, all the axioms and the theorem can be proved using GRIND. -Shankar

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

- Prev by Date:
**Re: instantiation** - Next by Date:
**Re: How to kill a runaway proof attempt?** - Prev by thread:
**Re: instantiation** - Next by thread:
**records** - Index(es):