论文标题
明确的公式，否定性和直觉命题逻辑的基础扩展语义
Definite Formulae, Negation-as-Failure, and the Base-extension Semantics of Intuitionistic Propositional Logic
论文作者
论文摘要
证明理论语义（P-TS）是语义的范式，其中逻辑中的含义基于证明（与真理相反）。直觉命题逻辑（IPL）的P-TS的特定实例是其基础扩展语义（B-ES）。该语义是由称为支持的关系给出的，解释了逻辑常数的含义，该逻辑常数由称为基础的规则系统来参数，这些规则提供了提供原子命题的语义的基础。在本文中，我们将基础解释为确定公式的集合，并使用统一证明搜索（逻辑编程的证明理论基础（LP）提供的后者的操作视图）来确定B-ES IPL的完整性。这种观点允许否定，这是P-TS中一个微妙的问题，可以从LP中的否定协议来理解。具体而言，尽管传统上将否定命题被理解为对其否定的主张，但在B-ES中，我们可能会理解对命题的拒绝是未能找到其证明的。这样，断言和否认都是P-TS中的主要概念。
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.
