computability, model-checking, and human reasoning

[gusl]

Halpern, Vardi - Model Checking vs Theorem-Proving: A Manifesto suggests model-checking as a cheaper alternative, since theorem-proving is NP-complete. This seems to me to be more like how humans reason, precisely for the same reason (unlike some people, I believe our brains are classical computers).

Towards a `Model Computation Manifesto'

Computability Logic