Specialized · a field of logic
Computational Logic
Logic programming and automated reasoning, logic made to run: Prolog, resolution, SAT, and the theorem provers.
An entry point for computer science
- The problem
- Which logical questions can a machine answer mechanically, and how do we make inference itself computable?
- The turning point
- Church’s λ-calculus and the undecidability of the halting problem fix the precise limit of mechanical reasoning.
- An open question
- How far can SAT/SMT solvers and proof assistants scale, and can machines find genuinely new proofs?
The Canon
- An Unsolvable Problem of Elementary Number Theory 1936
- Foundations of Logic Programming
- Handbook of Automated Reasoning
To study it
- The Art of Prolog
- First-Order Logic and Automated Theorem Proving