统一语义与语法推理限制的挑战
计算机科学中的逻辑
2020-01-01 v1
摘要
虽然语法推理限制在 SAT 中并不起重要作用，但对于更具表达力的逻辑（如的一阶逻辑或其片段）而言，它们是一种基本的推理技术。特别是，它们能够产生简短的证明或模型表示。另一方面，语义引导的推理系统享有重要的性质，例如仅生成非冗余子句。我讨论了这两种范式在多大程度上可以统一。
引用
@article{arxiv.1912.12966,
title = {The Challenge of Unifying Semantic and Syntactic Inference Restrictions},
author = {Christoph Weidenbach},
journal= {arXiv preprint arXiv:1912.12966},
year = {2020}
}
备注
In Proceedings ARCADE 2019, arXiv:1912.11786