search

advancedresearch / poi

a pragmatic point-free theorem prover assistant
Apache License 2.0
136 stars 7 forks source link

Is it possible for Poi to automatically find easily invertible formulas? #1093

Open bvssvni opened 9 months ago

bvssvni commented 9 months ago

One idea is to transform a formula into using a single symbol, e.g.:

x + x => 2 * x
x * x => x^2

It is easy to find the inverses inv(mul(2)) and inv((^ 2)).

Maybe there could be a command to transform a formula into a form which is easily invertible.