RichardMoot / LinearOne

LinearOne is a prototype theorem prover for first-order (multiplicative, intuitionistic) linear logic.
GNU Lesser General Public License v2.1
18 stars 2 forks source link

Add position constraints #25

Open RichardMoot opened 9 years ago

RichardMoot commented 9 years ago

Allow specification of constraints of the form X=<Y. These constraints will help with the treatment the reflexives of the Displacement calculus, but they are a simple and powerful mechanism in general.

The constraint-like implementation will essentially be the following X =< X <=> true X =< Y, integer(X), integer(Y) <=> Prolog's X =< Y for integers (evaluates to true or false) X =< Y, Y =<X <=> X = Y X =< Y, Y =< Z => X =< Z (only rule which adds constraint)