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

Dancing links #4

Closed RichardMoot closed 9 years ago

RichardMoot commented 9 years ago

Implement smarter axiom link strategy, selecting the axiom which has the least possible partner (similar to the Grail 3 strategy and to Knuth's general Dancing Links algorithm).

RichardMoot commented 9 years ago

Merged first version of dancing links into master branch. Some more improvements and testing are surely necessary, but for now this issue can be closed.