search

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

Select random #30

Closed RichardMoot closed 9 years ago

RichardMoot commented 9 years ago

Correction to the dancing links module, which caused some contractions of very "tangled" proof nets to result in (incorrect) failure.

Preparation for more flexible atom selection strategies.