advancedresearch / poi

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

Use Avalog as context solver #1061

Open bvssvni opened 3 years ago

bvssvni commented 3 years ago

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 conflicting information or inductive information might be stored in the context, this requires a monotonic solver with ambiguity checking.

I suggest using Avalog.