• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Symposium on Computer and Information Sciences(ISCIS 2004); 20041027-29; Kemer-Antalya(TR) >System BV without the Equalities for Unit
【24h】

System BV without the Equalities for Unit

机译：没有单位平等的系统BV

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

摘要

System BV is an extension of multiplicative linear logic with a non-commutative self-dual operator. In this paper, we present systems equivalent to system BV where equalities for unit are oriented from left to right and new structural rules are introduced to preserve completeness. While the first system allows units to appear in the structures, the second system makes it possible to completely remove the units from the language of BV by proving the normal forms of the structures that are provable in BV. The resulting systems provide a better performance in automated proof search by disabling redundant applications of inference rules due to the unit. As evidence, we provide a comparison of the performance of these systems in a Maude implementation.
机译：系统BV是具有非交换自对偶运算符的乘法线性逻辑的扩展。在本文中，我们介绍了与系统BV等效的系统，其中单位的均等性从左到右，并且引入了新的结构规则以保持完整性。第一个系统允许单元出现在结构中，而第二个系统则可以通过证明BV可证明的结构的正常形式，从BV语言中完全删除这些单元。通过禁用由于该单元导致的推理规则的冗余应用，所得的系统在自动证明搜索中提供了更好的性能。作为证据，我们提供了在Maude实现中这些系统性能的比较。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号