[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
critical-pairs, 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 50011-1040 USA / leavens@cs.iastate.edu
phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
URL: http://www.cs.iastate.edu/~leavens/homepage.html
Follow-Up(s):