Better constraints for forall links

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

Better constraints for forall links #14

Open RichardMoot opened 9 years ago

RichardMoot commented 9 years ago

Forall links have the property that no atom containing the eigenvariable of a link can every be identified with a node which dominates the forall link of this variable. Adding this constraint would reduce the search space and make testing the forall contraction less complicated.

RichardMoot commented 9 years ago

Besides the forall links, better constraints to reduce the search space are welcome anywhere