• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Negative Operations on Proofs and Labels
【24h】

Negative Operations on Proofs and Labels

机译：证明和标签的负运算

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Logic of proofs LP introduced by S. Artemov in 1995 describes properties of proof predicate 't is a proof of F' in the propositional language extended by atoms of the form [t]F. Proof are represented by terms constructed by three elementary recursive operations on proofs. In order to make the language more expressive we introduce the additional storage predicate with the intended interpretation 'x is a label for F'. It can play the role of syntax encoding, so it is useful for specification of operations that require formula arguments. In this paper we study operations on proofs and labels that can be specified in the extended language. First, we give a formal definition of an operation on proofs and labels. Then, for an arbitrary finite set of operations F the logic LPS(F) is defined. We provide LPS(F) with symbolic semantics and arithmetical semantics. The main result of the paper is the uniform completeness theorem for this family of logics with respect to the both types of semantics.
机译：S. Artemov在1995年提出的证明逻辑LP描述了命题语言“ t是F的证明”的性质，该命题语言由[t] F形式的原子扩展。证明由对证明的三个基本递归运算构成的术语表示。为了使语言更具表达力，我们引入了附加的存储谓词以及预期的解释“ x是F的标签”。它可以起到语法编码的作用，因此对于指定需要公式参数的操作很有用。在本文中，我们研究了可以用扩展语言指定的证明和标签的操作。首先，我们对证明和标签的操作进行正式定义。然后，对于任意有限的一组运算F，定义逻辑LPS（F）。我们为LPS（F）提供符号语义和算术语义。本文的主要结果是针对这两种语义的逻辑家族的统一完整性定理。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号