345 alternative exists unfolding #346
Open
Conversation
This file contains hidden or 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
Update the Exists().unfold() method and in the process fix some buggy code that seemed to assume that an Exists() object always has one or more explicit conditions. For now, the old code has been left in place, commented out, for comparison. Also update the logic/booleans/quantification/existence demonstrations.ipynb notebook with related testing of the new Exists().unfold() method.
Update the Exists().definition() method and in the process fix some buggy code that seemed to assume that an Exists() object always has one or more explicit conditions. Also update the logic/booleans/quantification/existence demonstrations.ipynb notebook with related testing of the new Exists().definition() method.
…-theory pkg Add two basic theorems to logic/booleans/quantification/existence sub-theory pkg, namely `exists_not_unfolding` and `exists_not_unfolding`, to complement/supplement the theorems already there and make it a little easier to go between an existence such that Not(P) and Not(Forall(P)). Corresponding Exists() methods or method updates not yet implemented.
Establish the exists_not_eq_not_forall theorem in logic/booleans/quantification/existence sub-theory package, being the Exists(x, Not(P(x))) analog to the Exists(x, P(x)) `exists_def' axiom.
Augment Exists().unfold() and Exists().definition() methods to also deal with the cases of Exists(x, Not(P(x))) instead of just the Exists(x, P(x)) cases, and establish some minimal testing of the methods in the existence demonstrations notebook. The augmentations utilize the alternative existential unfolding, folding, and equality theorems in recent previous commits.
Update exists.py, settling on the use of a preserve_all = True approach in the Exists().definition() method and cleaning out older code and comments.
Update the logic/booleans/quantification/existence demonstrations notebook, adding some example Exists() expressions to test and demonstrate recent updates to the existential theorems and related Exists() methods.
|
This branch adds a few Exists()-related theorems and updates several Exists() methods (fixing some bugs along the way), and updates the logic/booleans/quantification/existence demonstrations notebook to provide more demonstrations and testing. |
…pproach Update the Exists().definition() method to use a more specific expression-preservation approach instead of the 'preserve_all = True' approach. The 'preserve_all = True' leaves preserved the "empty" condition cases which then show up as a redundant 'T' in the eventual expression result; this more precise preservation method constructs the expected rhs expression and explicitly preserves that instead. This performs well in a handful of examples in the existence demonstrations notebook.
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.
No description provided.