4 1 Introduction
but this is not a first-order formula! Of course this is not a formal proof that
reachability is not expressible in first-order logic (we shall see a proof of this
fact in Chap. 3), but at least it gives a hint as to what the limitations of
first-order logic are.
The inability of first-order logic to express some important queries moti-
vated a lot of research on extensions of first-order logic that can do queries
such as transitive closure or cardinality comparisons. We shall see a number
of extensions of these kinds – fixed point logics, (fragments of) second-order
logic, counting logics – that are important for database theory, and we shall
study properties of these extensions as well.
1.2 An Example from Complexity Theory
We now turn to a different area, and to more expressive logics. Suppose that
we have a graph, this time undirected, given to us as a pair hV, Ei, where V
is the set of vertices, or nodes, and E is the edge relation. Assume that now
we can specify graph properties in second-order logic; that is, we can quantify
over sets (or relations) of nodes.
Consider a well-known property of Hamiltonicity. A simple circuit in a
graph G is a sequence (a
1
, . . . , a
n
) of distinct nodes such that there are
edges (a
1
, a
2
), (a
2
, a
3
), . . . , (a
n−1
, a
n
), (a
n
, a
1
). A simple circuit is Hamiltonian
if V = {a
1
, . . . , a
n
}. A graph is Hamiltonian if it has a Hamiltonian circuit.
We now consider the following formula:
∃L ∃S
linear order(L)
∧ S is the successor relation of L
∧ ∀x∃y (L(x, y) ∨ L(y, x))
∧ ∀x∀y (S(x, y) → E(x, y))
(1.1)
The quantifiers ∃L ∃S state the existence of two binary relations, L and S,
that satisfy the formula in parentheses. That formula uses some abbreviations.
The subformula linear order(L) in (1.1) states that the relation L is a linear
ordering; it can be defined as
∀x¬L(x, x)
∧
∀x∀y∀z (L(x, y) ∧L(y, z) → L(x, z))
∧ ∀x∀y
(x 6= y) →
L(x, y) ∨L(y, x)
.
The subformula S is the successor relation of L states that S is the successor
relation associated with the linear ordering L; it can be defined as
∀x∀y S(x, y) ↔
L(x, y) ∧ ¬∃z
L(x, z) ∧ L(z, y)
∨
¬∃z L(x, z) ∧ ¬∃z L(z, y)
!
剩余325页未读，继续阅读
Hilovaiseriliis
- 粉丝: 0
- 资源: 5
我的内容管理
展开
最新资源
- 解决本地连接丢失无法上网的问题
- BIOS报警声音解析：故障原因与解决方法
- 广义均值移动跟踪算法在视频目标跟踪中的应用研究
- C++Builder快捷键大全：高效编程的秘密武器
- 网页制作入门：常用代码详解
- TX2440A开发板网络远程监控系统移植教程：易搭建与通用解决方案
- WebLogic10虚拟内存配置详解与优化技巧
- C#网络编程深度解析：Socket基础与应用
- 掌握Struts1：Java MVC轻量级框架详解
- 20个必备CSS代码段提升Web开发效率
- CSS样式大全：字体、文本、列表样式详解
- Proteus元件库大全：从基础到高级组件
- 74HC08芯片：高速CMOS四输入与门详细资料
- C#获取当前路径的多种方法详解
- 修复MySQL乱码问题：设置字符集为GB2312
- C语言的诞生与演进：从汇编到系统编程的革命
资源上传下载、课程学习等过程中有任何疑问或建议，欢迎提出宝贵意见哦~我们会及时处理！
点击此处反馈
