search

statebox / cql

CQL: Categorical Query Language implementation in Haskell
GNU Affero General Public License v3.0
162 stars 14 forks source link

congruence prover #30

Closed wisnesky closed 5 years ago

wisnesky commented 5 years ago

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://www.lsi.upc.edu/~oliveras/espai/papers/IC.pdf .