5 ms·
Logic Solvers in JavaScript
- Tankenstein 12y agoThis is terrific! Speedy javascript as well.
- deadprogram 12y agoThis is very cool, good work!
- drostie 12y agoThere'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.
- tammet 12y agoYep, a bug has creeped into a preprocessor. Debugging right now :) thx!
- earleybird 12y agoThe author has been writing performant provers for a while :-) https://scholar.google.com/citations?user=ElzaeUYAAAAJ https://scholar.google.com/citations?user=ElzaeUYAAAAJ also Gandalf/Hobbit (SCM) http://www.cs.miami.edu/~tptp/CASC/19/SystemDescriptions.html#Gandalf---c-2.6 http://www.cs.miami.edu/~tptp/CASC/19/SystemDescriptions.htm...