Davis-Putnam Mode #87
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Co-Authored-By: Jody Sunray <[email protected]>
Co-Authored-By: Jenny Gao <[email protected]>
Co-Authored-By: Jenny Gao <[email protected]>
Co-Authored-By: Jenny Gao <[email protected]>
Co-Authored-By: Jenny Gao <[email protected]>
ToDo - add checks for when assertion gets absorbed by intermediate steps Co-Authored-By: Jody Sunray <[email protected]>
Co-Authored-By: Jenny Gao <[email protected]>
Co-Authored-By: Jody Sunray <[email protected]>
Co-Authored-By: Jody Sunray <[email protected]>
Add Modes to nav bar
Co-Authored-By: Jody Sunray <[email protected]>
ToDo: - validate (isDecomposed) - tauts will have too many things in decomposition array. ensure it stil validates Co-Authored-By: Jenny Gao <[email protected]>
- disabled calles to isDecomposed (will need to circle back) on these Co-Authored-By: Jody Sunray <[email protected]>
Co-Authored-By: Jody Sunray <[email protected]>
Co-Authored-By: Jody Sunray <[email protected]>
Co-Authored-By: Jenny Gao <[email protected]>
Co-Authored-By: Jody Sunray <[email protected]>
Co-Authored-By: Jody Sunray <[email protected]>
Co-Authored-By: Jenny Gao <[email protected]>
Davis Putnam Rules
- remove extraneous comments - add some comments - fix correctness error codes
also fixed issue related to branch literals (when checking the correctness of the tree, we weren't storing nodes in the decomposition of any literal, which was breaking the representation check)
TODO: make this only render if in DP mode
Branch literal labels, handle terminators, code cleanup
DP mode toggle
Co-Authored-By: Jenny Gao <[email protected]>
Co-Authored-By: Jenny Gao <[email protected]>
edited the validate function for closed terminator to allow for selection of two antecedents, as opposed to just the contradiction symbol
we have to clear out the antecedents array for statements in the deleted statement's decomposition
…o tautology_dp
|
Haven't had time to review this yet -- I'm taking a brief look now but nothing too in depth. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This feature was implemented as a final project by Jenny Gao (@jeninyg), Mason duBoef (@mduboef), and Jody Sunray (@jssunray34) for Bram van Heuveln's Spring 2023 Computability and Logic course at RPI.
Details about the implementation can be found here: https://github.com/Bram-Hub/Willow/blob/tautology_dp/DP_developer_guide.md.
A user guide for Davis-Putnam mode can be found here: https://github.com/Bram-Hub/Willow/blob/tautology_dp/DP_userguide.md.
We primarily used the following two trees to test our implementation: simple_open_branch_DP.willow and closed_branches_DP_hw4.willow.
Note: old
.willowfiles are no longer supported. This is due to DP statements having 2 antecedents (a parent statement and literal branch), changing the structure of the tree.