Hacker News Reader

> describe facts about some discrete system and check for the existence (or nonexistence) of properties

To me this sounds like Logic Programming and I immediately think of Prolog. Is it fair to compare them?

Yes, but the implementation is very different. These model checkers aren't turing complete, and because of that they can give some strong guarantees about what they can and cannot do. Prolog? Shift some things around and watch your program suddenly run forever or so slowly as to be useless.

If you want to mess around with something very prolog like but using similar kinds of underlying tech to these model checkers, try playing around with ASP solvers like Clingo/Clasp or DLV

Reply on news.ycombinator.com