Open wisnesky opened 5 years ago
I can't figure out how to attach files to these issues, so here's a paywalled link to the prover we need implemented: https://epubs.siam.org/doi/abs/10.1137/0214073
Java version: https://github.com/CategoricalData/fql/blob/master/src/main/java/catdata/provers/Thue.java
Once implemented, it then needs to be lifted from Thue systems to arbitrary AQL collages on free typesides, a la: https://github.com/CategoricalData/fql/blob/master/src/main/java/catdata/provers/MonoidalProver.java
This prover is AQL java's workhorse prover, selected almost all of the time.
I can't figure out how to attach files to these issues, so here's a paywalled link to the prover we need implemented: https://epubs.siam.org/doi/abs/10.1137/0214073
Java version: https://github.com/CategoricalData/fql/blob/master/src/main/java/catdata/provers/Thue.java
Once implemented, it then needs to be lifted from Thue systems to arbitrary AQL collages on free typesides, a la: https://github.com/CategoricalData/fql/blob/master/src/main/java/catdata/provers/MonoidalProver.java
This prover is AQL java's workhorse prover, selected almost all of the time.