Operations on `Theorem`s for forward-reasoning

GaloisInc / saw-script

The SAW scripting language.

BSD 3-Clause "New" or "Revised" License

438 stars 63 forks source link

Operations on `Theorem`s for forward-reasoning #91

Open brianhuffman opened 8 years ago

brianhuffman commented 8 years ago

Currently there's not much you can do in saw-script with a Theorem value: You can print it, and if it's an equation you can add it to a Simpset.

It would be nice to have some additional operations that would enable forward reasoning:

Rewriting of theorems with a Simpset
Instantiating universal quantifiers
Generalizing over symbolic variables
Modus ponens, i.e. implication elimination
Symmetry and transitivity of equation theorems

robdockins commented 3 years ago

There are at least experimental versions of many of these operations now. What still needs to be done to close this ticket?