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

Add/evaluate a choice of tie-breakers to the dancing links algorithm #13

Open RichardMoot opened 9 years ago

RichardMoot commented 9 years ago

One possible tie-breaker would be "commit", which, all other things being equal prefers nodes we have already connected (this would avoid back-and-forth between independent choices).

RichardMoot commented 9 years ago

Another possible tie-breaker would prefer the shorted distance between words in the graph (this would require more information to be stored at the atoms). This tie-breaker would be similar to the proof nets and human processing approaches of Johnson and Morrill