![](https://csdnimg.cn/release/download_crawler_static/10756392/bg4.jpg)
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