Proof-theoretic semantics (P-tS) is the paradigm of semantics in which meaning in logic is based on proof (as opposed to truth). A particular instance of P-tS for intuitionistic propositional logic (IPL) is its base-extension semantics (B-eS). This semantics is given by a relation called support, explaining the meaning of the logical constants, which is parameterized by systems of rules called bases that provide the semantics of atomic propositions. In this paper, we interpret bases as collections of definite formulae and use the operational view of the latter as provided by uniform proof-search -- the proof-theoretic foundation of logic programming (LP) -- to establish the completeness of IPL for the B-eS. This perspective allows negation, a subtle issue in P-tS, to be understood in terms of the negation-as-failure protocol in LP. Specifically, while the denial of a proposition is traditionally understood as the assertion of its negation, in B-eS we may understand the denial of a proposition as the failure to find a proof of it. In this way, assertion and denial are both prime concepts in P-tS.

翻译：证明论语义学（P-tS）是一种以证明（而非真理）作为逻辑意义基础的语义学范式。直觉主义命题逻辑（IPL）的证明论语义学具体表现为基扩展语义学（B-eS）。该语义学通过称为“支持”的关系来定义逻辑常项的意义，该关系以名为“基”的规则系统为参数，这些基为原子命题提供语义。本文中，我们将基解释为定式公式的集合，并利用统一证明搜索（逻辑编程LP的证明论基础）提供的操作性视角，建立IPL关于B-eS的完备性。这一视角使得证明论语义学中棘手的否定问题，能够通过逻辑编程中的“失败即否定”协议得以理解。具体而言，传统上对命题的否定被理解为对其否定的断言，而在B-eS中，我们可以将否定命题理解为未能找到其证明。由此，断言与否定成为证明论语义学中的两个原始概念。