Computer Science Logic
Computer Science Logic
复制标题
计算机科学逻辑
DOI：
10.1007/978-3-642-15205-4_34
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Nenov Y
中科院分区：
文献类型：
--
作者：
Nenov Y
通过欧氏逻辑，我们理解了一种形式语言，它的变量范围在欧氏空间的子集上，具有固定的维度，其非逻辑原语具有固定的含义，如涉及这些集合的几何性质、关系和运算。本文考虑具有原语的一阶欧几里得逻辑的连通性和凸性、接触的二元关系以及三元关系的紧性。当变量取值于一维、二维和三维空间的不同子集集合时，我们研究了相应的一阶理论的计算性质。我们证明了基于维大于1的欧几里德空间的理论都可以编码一阶或二阶算术，因此是不可判定的。我们证明，对于能够表达接近关系的逻辑，基于一维欧氏空间的结构理论具有与其高维对应的相同的复杂性。相比之下，在没有比它更接近的谓词的情况下，这里考虑的所有基于一维欧几里得空间的理论都是可判定的，但不是初等的。
By aEuclidean logic, we understand a formal language whose variables range over subsets of Euclidean space, of some fixed dimension, and whose non-logical primitives have fixed meanings as geometrical properties, relations and operations involving those sets. In this paper, we consider first-order Euclidean logics with primitives for the properties ofconnectednessandconvexity, the binary relation ofcontactand the ternary relation ofbeing closer-than. We investigate the computational properties of the corresponding first-order theories when variables are taken to range over various collections of subsets of 1-, 2- and 3-dimensional space. We show that the theories based on Euclidean spaces of dimension greater than 1 can all encode either first- or second-order arithmetic, and hence are undecidable. We show that, for logics able to express thecloser-thanrelation, the theories of structures based on 1-dimensional Euclidean space have the same complexities as their higher-dimensional counterparts. By contrast, in the absence of thecloser-thanpredicate, all of the theories based on 1-dimensional Euclidean space considered here are decidable, but non-elementary.
新的构造逻辑：经典逻辑
影响因子：
0.5
作者：
J. Girard
通讯作者：
J. Girard
公式作为类型的控制概念
DOI：
--
发表时间：
1989
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
T. Griffin
通讯作者：
T. Griffin