This paper is structured as follows: Section 2 explores closed-world and open-
world logic programs; it details previous attempts to integrate LP with decision
procedures. Section 3 presents the syntax and static semantics of a core open-
world language. Section 4 gives the logical semantics of OLPs and Section 5
formalizes execution and symbolic execution. We conclude in Section 6.
2 Extending LP Paradigms With Decision Procedures
Logic programming (LP) has long been used for formal specifications. It is attrac-
tive because it is precise, declarative, executable, and expressive (corresponding
to various classes of fixpoint logic). Its usefulness for formal specifications is
still vigorously researched, e.g. in the context of distributed systems [10], ac-
cess control logics [11, 12], and declarative databases [13]. However, existing LP
paradigms do not integrate well with the powerful decision procedures arising
from constraint solving. The problems are as follows: Prolog extended with con-
straints requires users to syntactically schedule constraint introduction. Conse-
quently, two specifications that appear equivalent may exhibit very different exe-
cutions. The Answer Set Programming (ASP) paradigm, based on stable models,
performs searches over finite groundings of programs. ASP makes only limited
use of decision procedures, and lacks generic support for infinite domains even
when decision procedures for these domains are available.
We now introduce closed-world and open-world logic programming, and give
a detailed account of existing LP paradigms and their integration with decision
procedures. In the interest of space, we shall study a small problem that chal-
lenges these paradigms. In the text to follow t is a vector of terms and t
i
is the
i
th
term of t. We write t[x\t] for the simultaneous replacement of variables x
i
with terms t
i
in t.
2.1 A Brief Summary Of Closed-World Logic Programs
A closed-world logic program contains a fixed set of rules. Each rule has the form
R(t) :- body. R(t) is called the head of the rule. R is a relation symbol called
a program relation. The body is a conjunction of constraints possibly containing
other program relations. Informally, whenever the body of a rule is satisfied for
some substitution of variables body[x\t
0
], then the relation R must be true for
all elements of the form t[x\t
0
]. Negation is the ability to test ¬R(t) in the body
of a rule. A fact is a rule whose body is empty; such a body is treated as true.
The exact semantics of programs vary between paradigms. We shall discuss this
in more detail in the following sections.
Program execution determines members of a relation R by applying rules. In
forward chaining the rules are repeatedly applied, starting from facts, building
up the elements of R. Execution terminates when no rule extends any relation
further, i.e. a least fixpoint is reached. Backwards chaining tries to prove that
some element of the form t is in R by working backwards through the rules,
from heads to bodies until reaching facts. A query operation on a closed-world
剩余18页未读，继续阅读
jtzwy
- 粉丝: 1
- 资源: 6
我的内容管理
展开
最新资源
- 新型矿用本安直流稳压电源设计：双重保护电路
- 煤矿掘进工作面安全因素研究：结构方程模型
- 利用同位素位移探测原子内部新型力
- 钻锚机钻臂动力学仿真分析与优化
- 钻孔成像技术在巷道松动圈检测与支护设计中的应用
- 极化与非极化ep碰撞中J/ψ的Sivers与cos2φ效应：理论分析与COMPASS验证
- 新疆矿区1200m深孔钻探关键技术与实践
- 建筑行业事故预防：综合动态事故致因理论的应用
- 北斗卫星监测系统在电网塔形实时监控中的应用
- 煤层气羽状水平井数值模拟：交替隐式算法的应用
- 开放字符串T对偶与双空间坐标变换
- 煤矿瓦斯抽采半径测定新方法——瓦斯储量法
- 大倾角大采高工作面设备稳定与安全控制关键技术
- 超标违规背景下的热波动影响分析
- 中国煤矿选煤设计进展与挑战：历史、现状与未来发展
- 反演技术与RBF神经网络在移动机器人控制中的应用
资源上传下载、课程学习等过程中有任何疑问或建议，欢迎提出宝贵意见哦~我们会及时处理！
点击此处反馈
