Logic Solvers in JavaScript

There's something seriously messed up with these algorithms. Take as input:

    a -> a

According to 'dpll: better' this is unsatisfiable. (It isn't; it's a tautology.) The algorithm 'dpll: naive' does not succeed either. The rest of the algorithms fail to observe it as a tautology and instead look for a specific input which makes it correct (generally 'a'). That's not necessarily a bad thing but it was somewhat unexpected (as when it gives you the solution you're probably tempted to think it's "the" solution and not just "a" solution) -- the easiest workaround is to look for the unsatisfiability of ~(a -> a).

Using this here is a counterexample to 'dpll: better' showing just how bad it is:

    ~((a -> b) -> (((a -> b) -> c) -> c))

"Clause set is true if we assign values to variables as: a b c".

(This is the negation of another tautology, saying that if we have access to a value of type x and a function from x -> y then we have access to a value of type y. The only complication is that x is a function from a -> b and y is labeled c.)

A famous tautology which is not available to type theory is Pierce's law,

    ((p -> q) -> p) -> p

'dpll: better' also says that this is unsatisfiable, but also that its negation is unsatisfiable.

The author has been writing performant provers for a while :-)

https://scholar.google.com/citations?user=ElzaeUYAAAAJ

also Gandalf/Hobbit (SCM) http://www.cs.miami.edu/~tptp/CASC/19/SystemDescriptions.htm...

This is terrific! Speedy javascript as well.

This is very cool, good work!