Model-theoretic semantics comes with a computational counterpart: to check validity is to search for a countermodel, and tableaux, resolution, and satisfiability solvers make the semantics something one can run. Proof-theoretic semantics -- the younger paradigm in which meaning is given by inferential role rather than by denotation -- has no established counterpart. This paper proposes one: logic programming. We show that Sandqvist's base-extension semantics for intuitionistic propositional logic is executable in a precise sense. Bases are logic programs, and to each formula $\varphi$ we assign a goal $[\![\varphi]\!]$ of a second-order hereditary Harrop language such that $\varphi$ is supported in a base $\mathcal{B}$ exactly when $[\![\varphi]\!]$ is operationally derivable from $\mathcal{B}$ read as a program. The encoding is the Russell-Prawitz translation of the connectives with quantification restricted to atoms, and this restriction is not a limitation but the point: it is what the support clauses themselves demand. The correspondence is exact base by base, not merely at the level of validity, so that intuitionistic validity becomes the success of a single query against the empty program. Logic programming stands to proof-theoretic semantics as tableaux and satisfiability solvers stand to model-theoretic semantics.

翻译：暂无翻译