Problem solving and theorem proving
Christopher John Hogger · 1990
Abstract The problem-solving mechanism of logic programming is fundamentally a theorem proving (inferential) mechanism. As indicated earlier in the course, our aim is to characterize computation as the inference-driven manipulation of knowledge. More concretely, the interpreters that we employ to execute logic programs are just automated theorem provers, so that we might expect proof theory to tell us something about their capabilities and limitations.