search

Brandon-Rozek / vspursuer

Verify Relevance Properties for Matrix Models with Implicative Connectives
3 stars 0 forks source link

Non-deterministic Completeness Bug #20

Closed Brandon-Rozek closed 5 hours ago

Brandon-Rozek commented 5 hours ago

Testing the logic B plus p → (p → p) and (p → (q → r )) → (q → (p → r )) leads to sometimes the model 6.2.1.1.1 not having VSP

Brandon-Rozek commented 5 hours ago

This is due to an incorrect implementation of finding the top and bottom of the order