You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I like the current design of Hooo, because it is low level enough to keep the entire language in your head.
However, it would be nice to have more support when doing theorem proving.
Avalog (https://github.com/advancedresearch/avalog) uses the monotonic solver, but adds diagonalization to not get stuck on infinite theories. This would be nice to have this in Hooo, but I am not sure it is needed to help with simple theorem proving. One alternative is to use Avalog instead of the monotonic solver directly. This requires mapping the Avalog AST and translating proofs back to Hooo AST. I'm not sure whether that's something I would like to do.
Hooo already has in some sense a nice data structure for proofs. I believe a lot of easy assistance can be done by simple manipulations of this data structure. Possibly, a linear solver could be used (https://github.com/advancedresearch/linear_solver). For example, it could keep the data structure as one item and doing the reasoning by expanding out other facts, that gets eliminated and integrated when the goal is reached.
I would like to have a nice Rust API for assistance in Hooo, so that I can easily program my own automated theorem provers. Possibly, one could design a trait for theorem proving assistance and compile Hooo with different tools when needed. Hooo could ship with some nice tools by default.
I believe that having a simple API, AST and syntax is key to good design, while leveraging the ecosystem. My design philosophy of Hooo is that it is like code to be maintained over time. Avalog uses a different philosophy where it is basically more like data. Perhaps I can use Avalog. Perhaps even Dyon (https://github.com/pistondevelopers/dyon), but right now I'm just thinking about how to add some basic support.
The text was updated successfully, but these errors were encountered:
I like the current design of Hooo, because it is low level enough to keep the entire language in your head.
However, it would be nice to have more support when doing theorem proving.
The monotonic solver library (https://github.com/advancedresearch/monotonic_solver) supports both finding proofs and reducing proofs automatically.
Avalog (https://github.com/advancedresearch/avalog) uses the monotonic solver, but adds diagonalization to not get stuck on infinite theories. This would be nice to have this in Hooo, but I am not sure it is needed to help with simple theorem proving. One alternative is to use Avalog instead of the monotonic solver directly. This requires mapping the Avalog AST and translating proofs back to Hooo AST. I'm not sure whether that's something I would like to do.
Hooo already has in some sense a nice data structure for proofs. I believe a lot of easy assistance can be done by simple manipulations of this data structure. Possibly, a linear solver could be used (https://github.com/advancedresearch/linear_solver). For example, it could keep the data structure as one item and doing the reasoning by expanding out other facts, that gets eliminated and integrated when the goal is reached.
I would like to have a nice Rust API for assistance in Hooo, so that I can easily program my own automated theorem provers. Possibly, one could design a trait for theorem proving assistance and compile Hooo with different tools when needed. Hooo could ship with some nice tools by default.
I believe that having a simple API, AST and syntax is key to good design, while leveraging the ecosystem. My design philosophy of Hooo is that it is like code to be maintained over time. Avalog uses a different philosophy where it is basically more like data. Perhaps I can use Avalog. Perhaps even Dyon (https://github.com/pistondevelopers/dyon), but right now I'm just thinking about how to add some basic support.
The text was updated successfully, but these errors were encountered: