Prove-It
Prove-It copied to clipboard
sandialabs
A tool for proving and organizing general theorems using Python.
Currently, one needs to 'preserve_all' for all but the last step and this can get tricky. It would be slightly less efficient but easier to handle auto_simplify and replacements in...
Rather than ensuring sub-expressions are identical in order to cancel them (in a sum or product/division), we can do this based upon canonical forms. This has been implemented for Add...
Doing this properly should simplify transitive relation searches, making them more efficient. The idea would be to use canonical forms just for searching for known relations, equating things with the...
Deepak has always objected to "side-effects" as they have a negative connotation in formal methods. I do think "incidentals" is an appropriate name. Instead of a "side_effects" Expression method, we...
That's because whether or not a side-effect proof of one assumption happens first can determine whether a side-effect of another assumption follows through. For example, assumptions: (n in N+, x...
We could make the automation more powerful by integrating equivalence classes into the concept of using canonical forms. Note that this would depend upon assumptions and what has been proven,...
The order in which default attributes are updated makes a difference, and in particular the order in which replacements vs. preserved_exprs are updated/processed can make a difference when there is...
We can add a third category of statements to our theory packages: conservative definitions in addition to axioms and theorems. Many of our axioms could move over to the “conservative...
Instantiations are stored and reused for efficiency. However, these should sometimes be invalidated when autosimplification is used and simplification directives change.
Metadata
Owner
Metadata
A tool for proving and organizing general theorems using Python.