Sort It Out with Monotonicity - Translating between Many-Sorted and Unsorted First-Order Logic
Sort It Out with Monotonicity - Translating between Many-Sorted and Unsorted First-Order Logic
复制标题
以单调性对其进行排序 - 在多排序和未排序的一阶逻辑之间进行转换
DOI：
10.1007/978-3-642-22438-6_17
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Nicholas Smallbone
中科院分区：
文献类型：
--
作者：
Koen Claessen;A. Lillieström;Nicholas Smallbone
我们为分类逻辑提供了新的分析，该分析确定给定排序是否单调。单调排序的域总是可以用额外的元素扩展。我们使用此分析来显着改善未分类和多排序逻辑之间的众所周知的翻译，利用这一事实比非单调酮相比，翻译单调的翻译要便宜。许多有趣的问题在多组的一阶逻辑中更自然地表达，而不是在未分类的逻辑中，但是大多数现有高效的自动化定理掠夺者仅在未分类的逻辑中解决问题。相反，某些推理工具，例如模型查找器，可以很好地利用问题中的排序信息，但是当今的大多数问题都是以未分类的逻辑提出的。这种情况激发了多种方式和未分类问题之间的翻译。我们介绍了单调性分析及其在我们的工具单调毒素中的实现，并在TPTP基准库中显示了实验结果。
We present a novel analysis for sorted logic, which determines if a given sort is monotone. The domain of a monotone sort can always be extended with an extra element. We use this analysis to significantly improve well-known translations between unsorted and many-sorted logic, making use of the fact that it is cheaper to translate monotone sorts than non-monotone sorts. Many interesting problems are more naturally expressed in many-sorted first-order logic than in unsorted logic, but most existing highly-efficient automated theorem provers solve problems only in unsorted logic. Conversely, some reasoning tools, for example model finders, can make good use of sort-information in a problem, but most problems today are formulated in unsorted logic. This situation motivates translations in both ways between many-sorted and unsorted problems. We present the monotonicity analysis and its implementation in our tool Monotonox, and also show experimental results on the TPTP benchmark library.
DOI：
10.1007/s10817-011-9234-1
发表时间：
2011
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Alexander Krauss
通讯作者：
Alexander Krauss