congruence prover

[wisnesky]

No description provided.

[wisnesky]

In Prover.hs there is a datatype

data ProverName = Free | Congruence | Orthogonal | KB | Auto

Free and Orthogonal are already implemented. The goal here is to implement Congruence (i.e., fill in all existing missing case statements for ProverName) using the CongruenceClosure library:

https://hackage.haskell.org/package/toysolver-0.0.4/src/src/Algorithm/CongruenceClosure.hs

Also, a suitable example should be added to the test suite - and also the AQL java suite (email Ryan).

This will require both "currying" terms and flattening them to height three by introducing new symbols, as described in http:https://www.lsi.upc.edu/~oliveras/espai/papers/IC.pdf .