rairlab / lazyslate Goto Github PK

This is incorrect.

I am aware this does not work on firefox. It has something to do with the HTML5 canvas drawing differences.

Assumptions with the same name clash, should be based off of proof node IDs which are globally unique.

Example:

Proof:
https://james-oswald.github.io/lazyslate/?proof=N4Igdg9gJgpgziAXAbVASykgDAGnAQwFsYkQA5ImAQRDxgA8AHAJ3jjQjFJrwCsBXOABc0AMzQBjfCM6l8cOP2K0QjCOxldEoekgCsWAIx4AnkgBMevQF9rOdJkTGCyxOUo8QDFmw5aQAEIqAsJiktJ+cgpKJHhqGpHaILqIAOyGuCBmiJYALLb2IBgWeGCUpOYq3qwKiSAAFPhgUAAEVC0BAJTBgiLiUppyzQCSKvFog0kpegCcABymSLkAzHO2ALp4ADZoYADWCCjIuOabyMan69ZAA

This should fail but works.

Proof:
https://james-oswald.github.io/lazyslate/?proof=N4Igdg9gJgpgziAXAbVASykgjAGnAQwFsYkQsQ8YAPABwCd440IxSAKNAMwAJ9uBjAJQUQAKwCucAC5c0%2DfDJal8cOOOIiaEJotaJQVJAFYAnCbwBPJACYAzAA4Avo5zpMia3jBESiENZFqekZmPRAAIxEJaVl5XVIuAFFNbTR4%2DRBDRCNbABZLJFyAdixnVxAMQq8fKpAghlVQ5SjJGU45BSa%2DFTUNPC0dLoNC+1sCj1sisrdjao0%2DI0DaBqYlP0i8aLaO9JAe9RJ+1PThxHtcgAZxuymXGcQANjnfEAel4Ma1kA4ecN5hTatWKdL77PogAZpIaZJAmIz2a62WzTCruIrPUhFd4rLp7FoxdpxXFJFKDNanez2K4gKyIXK5IzOAC6eAANmgwABrBAoZD5aws5BGHBFQVPUU4ZC4AVMxxAA

https://james-oswald.github.io/lazyslate/?proof=N4Igdg9gJgpgziAXAbVASykgDAGnAQwFsYkQsQ8YAPABwCd440IxSaKQArAVzgBc0AMzQBjfAJal8cON2IcaEJhNaJQVJADZNuEAE8kAJgAcxgL5mc6TIgCMeMERKIQtjtXqNmqkAAohAAQ0AQCOAJQcPPxCouLeUjJyJHiKyvFqIBqIAOyahngGiCbZFlYgGEYOTqSG7rQMMukgIZG8AsJiKqRCAKIKSmhdGVnZtpoFSAAsAMyGpdZTVfIuk3WejZIuvpB8Ab4QdEGhYRF4Ue2xQyDSsvIpA0PqSLZYAKz5+lPTk%2DPlNq9LZwgV5rBpMTbNVrRDpxCE3JL9NKbJ6IACcr2mEyKxlsvwqiHGBGWIE0oK8EP2h2C4ShF06TQOAElEYN0ijUTMsTNcZYFjlAaRsmSNj5thBdjSzm0YvSITtmfckaoUS8sMYsa9jHNeX8kOqiUDjMLwaLAv5BEdwsdaTLYT4hAqQKlWcjMlpsvrCprXhYALp4AA2aDAAGsEChkPZDP7kLhozhkADNDHxtkY5McGmE%2DljL7fWYgA

Fails on:

Uncaught TypeError: node.add is not a function
at verifyIfIntro (verify.js:172:18)
at verifyNode (verify.js:22:20)
at verifyNodes (state.js:47:21)
at createLink (state.js:67:5)
at HTMLCanvasElement.onMouseDown (proofCanvas.js:88:17)

This Should work:

Link:
https://james-oswald.github.io/lazyslate/?proof=N4Igdg9gJgpgziAXAbVASykgDAGnAQwFsYkQsQ8YAPABwCd440IxSAKCOgAgEEuAhAJQUQAKwCucAC5oAZmgDG+GS1L44cccRE0ITFa0SgqSAGxYAHHgCeSAMx2LAXyc50mRAEY8YIiUQgniLU9IzMhiA8IhLScorK4WoaWiR4uvqJRiAmiADsAJy5NkieACx2Lm4gGEgATD5+pLXBtAwamSD80ZIy8koGSZraaXpoA1k5+QCsU8VepViV7kizBNoBUy2h7aoBHNx8Qt2xfQm7IJwAojqj48ZIuQVzU57Orst5DesguVttTOd9rwBMI8DFevFxhc6ABJG4ZXb3PIWXAgWyIOylTxLaoeKxrfwgCx%2DMKAzjAo5gnpxfodThwkYIwxI%2DKlepo+yOFwAXTwABs0GAANYIFDIXBTXnIby5KX1CxSoqSnDIKyS7lOIA

This is illegal, but marked as legal by the S-Expression Parser

Currently verification for rules with multiple parents is done in a hacky way where for each node we do a search over all parent's formula to determine if it is the correct form. For an example see the following code where we need to compute the left and right parents individually.

https://github.com/James-Oswald/lazyslate/blob/master/src/core/Proof/verify.ts#L242C15-L261

This type code is the source of many bugs (including #8). A better way to write this would be to generalize by writing a verification method for each rule that assumes the Premise proof nodes are passed in in a given order, just like how the real inference rules work. With this we can then try to verify all permutations of the premises, if just one of these verifies than the node verifies, otherwise if none of the permutations verify the node does not verify.

Additionally, this method probably does not sacrifice efficiency over the current version. Or Elim, the largest rule, only has 6 permutations of parents, and the code already basically checks these inside of the current verification function.