[Prev][Next][Index]
how to get LP to prove things like ~(1 <= 0) and (0 <= 2)?

Subject: how to get LP to prove things like ~(1 <= 0) and (0 <= 2)?

From: leavens@cs.iastate.edu (Gary Leavens)

Date: 6 Sep 95 18:14:42 GMT

Distribution: world

Keywords: LP, DecimalLiterals

Newsgroups: comp.specification.larch

Organization: Iowa State University, Ames, Iowa
I'm trying to use LP, so I can teach my students about it.
So please forgive this question (which should probably be a FAQ).
I'm using a few traits that make use of the LSL trait Integer,
and I always seem to run into proofs that require me to show
facts like ~(1 <= 0) and (0 <= 2). But I can't figure out
what to say to LP about this. (I guess it's something with
criticalpairs, but I'm not sure what?)
Here's the trait if you want to try it yourself...
%%%%%%%%%%%%%%%%%%%%%%
DecimalProblem: trait
includes Integer
implies
equations
~(1 <= 0);
0 <= 2;
%%%%%%%%%%%%%%%%%
Any help would be appreciated.
Gary

229 Atanasoff Hall, Department of Computer Science
Iowa State Univ., Ames, Iowa 500111040 USA / leavens@cs.iastate.edu
phone: (515)2941580 fax: (515)2940258 ftp site: ftp.cs.iastate.edu
URL: http://www.cs.iastate.edu/~leavens/homepage.html
FollowUp(s):