I'm curious about what HN thinks of answer set programming - the de facto language is a Prolog variant but in most implementations solutions are found by reducing programs to SAT instances. Upshot is you can reason about belief in an open world.