首页> 外文期刊>Journal of logic and computation >Interpolation in propositional Horn logic
【24h】

Interpolation in propositional Horn logic

机译:命题霍恩逻辑中的插值

获取原文
获取原文并翻译 | 示例
       

摘要

In this paper we give an abstract representation of propositional Horn logic (finite or infinitary) in terms of set-valued functions F : (sic) (PR) - (sic) (PR); here PR is the collection of atomic propositions. We investigate the properties of set-valued functions and establish that they satisfy the axioms of weak lazy Kleene algebra. These axioms and other properties are used to prove uniform left interpolation for propositional Horn logic. Then we introduce thin set-valued functions, which enable us to prove polynomial interpolation for propositional Horn logic. For the infinite case, the Axiom of Choice is used.
机译:在本文中,我们以集合值函数F:(sic)(PR)->(sic)(PR)给出命题Horn逻辑(有限或不定式)的抽象表示。 PR是原子命题的集合。我们研究了集值函数的性质,并确定它们满足弱懒惰Kleene代数的公理。这些公理和其他属性用于证明命题Horn逻辑的均匀左插值。然后,我们介绍了薄集值函数,这些函数使我们能够证明命题Horn逻辑的多项式插值。对于无限的情况,使用选择公理。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号