[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
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):