• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >Factor Varieties and Symbolic Computation
【24h】

Factor Varieties and Symbolic Computation

机译：因子种类和符号计算

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We propose an algebraization of classical and non-classical logics, based on factor varieties and decomposition operators. In particular, we provide a new method for determining whether a propositional formula is a tautology or a contradiction. This method can be automatized by defining a term rewriting system that enjoys confluence and strong normalization. This also suggests an original notion of logical gate and circuit, where propositional variables becomes logical gates and logical operations are implemented by substitution. Concerning formulas with quantifiers, we present a simple algorithm based on factor varieties for reducing first-order classical logic to equational logic. We achieve a completeness result for first-order classical logic without requiring any additional structure.
机译：我们建议基于因子变体和分解算子对经典逻辑和非经典逻辑进行代数化。特别是，我们提供了一种确定命题公式是重言式还是矛盾性的新方法。可以通过定义术语融合系统来自动实现此方法，该术语融合系统具有合流性和强大的标准化能力。这也暗示了逻辑门和电路的原始概念，其中命题变量变为逻辑门，逻辑运算通过替换实现。关于带有量词的公式，我们提出了一种基于因子变型的简单算法，用于将一阶经典逻辑简化为方程式逻辑。我们无需任何其他结构即可获得一阶经典逻辑的完整性结果。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号