poi

poi copied to clipboard

Currently, this is not possible to express. Add: - [ ] `inv((* \k:(!= 0))) => (/ k)` - [ ] `inv((/ \k:(!= 0))) => (* k)`

bvssvni

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...

bvssvni

bvssvni

Remove `eqb => eq`

2

An alternative to adding a [context solver](https://github.com/advancedresearch/poi/issues/1061) is separating `eqb` and `eq`. This means `eqb => eq` must be removed. However, `eq{(: bool), (: bool)}` might be used instead.

bvssvni

Currently, this can't be directly expressed.

bvssvni

`prime and . (not . ∃mul{(!= 1), (!= 1)}, (!= 1))`

bvssvni

Currently, there are some soundness problems due to Poi not being able to tell different types apart. These problems can be solved by storing information in the context. However, since...

bvssvni

Sometimes you want to find a constructive proof if possible and/or compare it to proofs with decidable propositions.

bvssvni

bvssvni

Currently the 4-value logic `true/false/both/neither` only works for Catuṣkoṭi existential lift. One idea is to extend the `true/false/both/neither` to all Boolean operations.

bvssvni