Look into first order logic reasoning engines

It looks like z3 cannot prove even very simple unequivalence with ForAll (https://git.science.uu.nl/d.h.ogilvie2/javawlp/commit/9f58f2ce85189f2995075801d49f0da6f5e2d55b#abb63567c9d6fd227500c8306dbe43002f6c8612_0_35)

Possible alternative engines to use:

• https://hackage.haskell.org/package/prolog
• http://src.seereason.com/chiou-prover/report.ps report.pdf
• https://hackage.haskell.org/package/Folly
• https://hackage.haskell.org/package/logic-classes
• https://github.com/daijo/fol
• https://github.com/dillonhuff/Folly

Perhaps some of these could be implemented as a LogicIR.Backend

changed the description

changed the description

changed the description

added research label

changed the description

changed title from look into first order logic reasoning engines to Look into first order logic reasoning engines

There appear to be no problems left with Z3 so this is no longer required.

closed