使用指南：gringo, clasp, clingo与iclingo在Answer Set Programming中的应用

需积分: 10 153 浏览量更新于2024-07-22 1 收藏 772KB PDF 举报

"A guide to gringo, clingo, and clasp, iclingo" 这篇文档是关于Answer Set Programming (ASP)工具的用户指南，包括gringo、clasp、clingo和iclingo，这些工具由波茨坦大学开发。gringo是一个归约器，能够将用户提供的逻辑程序转化为等价的命题逻辑程序。clasp则是一个求解器，用于计算此类程序的答案集。clingo将gringo的归约和clasp的求解功能整合在一起，形成一个用于用户程序的单一体系求解器。最后，iclingo通过增量模式扩展了clingo的功能，同时包含了归约和求解，使得处理过程更加高效。 1. **Answer Set Programming (ASP)简介** ASP是一种基于逻辑的编程范式，常用于复杂问题的求解，如规划、推理和知识表示。它允许用户用一种高级形式来表达问题，并通过寻找程序的“答案集”来解决问题。 2. **gringo：逻辑程序的归约器** gringo接受用户定义的逻辑程序，将其转化为布尔形式的命题逻辑程序，这个过程称为归约。归约是ASP系统中的关键步骤，因为它是将高级逻辑转换为可求解的形式。 3. **clasp：答案集求解器** clasp是用来计算归约后逻辑程序的答案集的工具。答案集是满足程序规则的所有可能解释，这些解释对应于问题的潜在解决方案。 4. **clingo：一体化求解器** clingo结合了gringo和clasp的功能，可以直接处理用户输入的逻辑程序，无需预先进行归约，大大简化了使用流程。 5. **iclingo：增量模式** iclingo增加了增量处理能力，允许在已有模型的基础上逐步添加或修改规则，这种特性在处理大规模问题或者动态更新问题时特别有用，能有效减少计算时间和资源消耗。 6. **应用领域** 这些工具在机器人大赛和解决数独等问题中都有应用，展示了其在人工智能领域的实用性。它们不仅适用于学术研究，也适合实际问题的解决，如机器人路径规划、智能决策和优化问题等。 7. **使用指南与功能参考** 文档旨在帮助ASP初学者理解和使用这些工具，同时也为经验丰富的用户提供了一种探索其高级特性的参考。通过以上介绍，我们可以看出gringo、clasp、clingo和iclingo是强大的ASP工具，它们提供了一套完整的解决方案，从逻辑程序的表示到问题的求解，为复杂问题的建模和求解提供了有力支持。这些工具的灵活性和效率使其成为人工智能和机器人领域的重要工具。

Essentially, the reduct relative to X is obtained by replacing all maximal unsatisﬁed

subformulas of F with ⊥. As a matter fact, this implies that any maximal negative

subformula of the form (G → ⊥) is replaced by either ⊥ (if X |= G) or (⊥ → ⊥) = >

(if X 6|= G). Furthermore, any atom occurring in F

belongs to X.

A propositional theory Φ is a set of propositional formulas, and the reduct of Φ

relative to a set X of atoms is Φ

= {F

| F ∈ Φ}. Furthermore, X is a model of Φ

if X |= F for every F ∈ Φ. Finally, X is an answer set of Φ if X is a ⊆-minimal model

of Φ

, that is, if X is a model of Φ such that no Y ⊂ X is a model of Φ

. The latter

condition uses the fact that X is a model of Φ

iff X is a model of Φ.

Also note that,

if X is an answer set of Φ, it is the unique ⊆-minimal model of Φ

because all atoms

occurring in Φ

belong to X (which excludes incomparable ⊆-minimal models). This

must not be confused with uniqueness of an answer set of Φ. In fact, Φ may have zero,

one, or multiple answer sets X (being ⊆-minimal models of distinct reducts Φ

). In

a sense, the ⊆-minimality of an answer set X as a model of Φ

stipulates the atoms

in X to be justiﬁed by Φ (or necessarily true) under the assumption of X.

For a logic program Π, answer sets of Π can now be explained by translation to a

propositional theory Φ[Π]. To this end, let

• Φ[Π] =

r∈ground(Π)

φ[r],

• φ[Head :- Body.] = (φ[Body] → ψ[Head ]),

• φ[A] = ψ[A] = A if A ∈ A,

• φ[>] = >,

• φ[not F ] = ¬φ[F ], and

• φ[G,H] = (φ[G] ∧ φ[H]).

The translation φ of a rule primarily consists of straightforward syntactic conversions

by replacing “:-,” “,,” and “not” with →, ∧, and ¬, respectively. However, it also

contains a separate translation ψ for heads of rules, which coincides with φ on atoms

by simply keeping them unchanged. In Section 4.1.10, we will customize ψ in order

to reﬂect the “choice semantics” for aggregates in heads of rules [25, 66]. By virtue of

the above translation, we can simply deﬁne the answer sets of a logic program Π to be

the answer sets of Φ[Π]. We have thus speciﬁed answer sets for normal programs.

In order to provide more intuitions, we now reproduce a direct deﬁnition of answer

sets for normal programs. This deﬁnition builds on the fact that the reduct for a normal

program is a set of Horn clauses, for which the ⊆-minimal model (if it exists) can

be constructed systematically in a bottom-up manner [14]. To this end, for a normal

program Π and a set X ⊆ ground(A), we deﬁne:

• T

Π,X

= ∅ and

• T

i+1

Π,X

= {head (r) | r ∈ ground (Π), body

(r) ⊆ T

Π,X

, body

−

(r) ∩ X = ∅}.

It is not hard to check that operator T

Π,X

is monotonic, as it adds head atoms of ground

rules to its previous result if the positive body atoms have been derived, while negative

bodies are merely evaluated w.r.t. X. Using this operator, we can equivalently deﬁne

X ⊆ ground (A) as an answer set of a normal program Π if X =

0≤i

Π,X

. This

equilibrium requirement exhibits two fundamental aspects of answer set semantics:

If X is not a model of Φ, then there is some F ∈ Φ such that X 6|= F , which in turn implies ⊥ ∈ Φ

Recall that a fact Head . is a shorthand for Head :- >.

1. Negative conditions are ﬁrst evaluated w.r.t. an answer set candidate.

2. The candidate must be justiﬁed by the result of the preceding evaluation.

Provided that X is a model of Π (that is, of Φ[Π]), the second item can be understood

in the sense that all atoms of X must have a proof from normal program Π w.r.t. X.

Example 2.4. The normal program in Example 2.1 (or its ground instantiation given

in Example 2.2) translates into the following propositional theory:

1 bird(tux) penguin(tux)

2 bird(tweety) chicken(tweety)

3 bird(tux) ∧ ¬neg_flies(tux) → flies(tux)

4 bird(tweety) ∧ ¬neg_flies(tweety) → flies(tweety)

5 bird(tux) ∧ ¬flies(tux) → neg_flies(tux)

6 bird(tweety) ∧ ¬flies(tweety) → neg_flies(tweety)

7 penguin(tux) → neg_flies(tux)

8 penguin(tweety) → neg_flies(tweety)

Let X = {bird(tux), penguin(tux), bird(tweety), chicken(tweety),

neg flies(tux), flies(tweety)}. Relative to X, we obtain the reduct:

1 bird(tux) penguin(tux)

2 bird(tweety) chicken(tweety)

3 ⊥ → ⊥

4 bird(tweety) ∧ > → flies(tweety)

5 bird(tux) ∧ > → neg_flies(tux)

6 ⊥ → ⊥

7 penguin(tux) → neg_flies(tux)

8 ⊥ → ⊥

We have that X is a model of the reduct (and the original program) because the reduct

does not contain formula ⊥ as an element. In addition, observe that no proper subset

of X is a model of the reduct. From this, we conclude that X is an answer set.

The latter can also be veriﬁed by determining

0≤i

Π,X

(for Π as in Example 2.1):

i T

Π,X

0 —

bird(tux), penguin(tux), bird(tweety), chicken(tweety)

bird(tux), penguin(tux), bird(tweety), chicken(tweety),

neg flies(tux), flies(tweety)

> 2 do.

For i = 1, we simply derive the head atoms of facts. They allow us to derive the re-

maining atoms of X, viz., neg flies(tux) and flies(tweety), in step i = 2.

In fact, two rules produce neg flies(tux), while

flies(tweety) :- bird(tweety), not neg_flies(tweety).

is the unique rule with head flies(tweety) that “ﬁres.” No further rules apply in

step i = 3, so that the set of atoms derived for i = 2 equals

0≤i

Π,X

. We have thus

reproduced X by bottom-up derivation, which again shows that X is an answer set. 

We have above seen two deﬁnitions of answer sets that start from an answer set

candidate X ⊆ ground (A), which is then veriﬁed in some way. Such deﬁnitions must

not be confused with the computation of answer sets, as (explicitly) enumerating all

subsets of ground(A) is infeasible in practice. Rather, the computational schemes

of solvers are similar to the “Davis-Putnam-Logemann-Loveland” procedure (DPLL)

[11, 12] or to “Conﬂict-Driven Clause Learning” (CDCL) [51, 54, 55].

3 Restrictedness Notions

In view of function symbols with non-zero arity, we may be confronted with logic

programs over an inﬁnite Herbrand base. In order to maintain decidability of reasoning

tasks, it is thus important to identify language fragments for which ﬁnite equivalent

ground programs are guaranteed to exist. Level-restricted logic programs constitute

such a fragment, where ﬁniteness is manifested in the requirement that any variable

in a rule must be bound to a ﬁnite set of ground terms via a predicate not subject to

positive recursion through that rule. The notion of level-restrictedness is complemented

by stratiﬁcation, which by disallowing negative recursion among predicates describes

a class of logic programs having unique answer sets. The formal deﬁnition of level-

restricted programs, which can be grounded by gringo (stand-alone or embedded in

clingo and iclingo), is provided in Section 3.1. Section 3.2 introduces stratiﬁed

programs and the related concept of domain predicates, which can serve particular

purposes during grounding. Both sections may be skimmed or even skipped upon the

ﬁrst reading, and rather be looked up later on to ﬁnd out details.

3.1 Level-Restricted Logic Programs

The main task of a grounder is to substitute the variables in a logic program Π by terms

such that the result is a ﬁnite equivalent ground program Π.

Of course, a necessary

condition for this is that Π possesses only ﬁnitely many ﬁnite answer sets. Unfortu-

nately, such a property is undecidable in general [10]. Instead of semantic properties,

grounders do thus impose rather simple syntactic conditions to guarantee the existence

of ﬁnite equivalent ground programs (which are then also computed). For instance, the

dlv system [43] requires programs to be safe for establishing ﬁniteness in the absence

of functions with non-zero arity and under limited arithmetic. Grounder lparse [68]

deals with ω-restricted programs [69], which are more restrictive than safe programs

but guarantee ﬁniteness also in the presence of functions with non-zero arity. Finally,

gringo [33] requires programs to be λ-restricted, a property more general than ω-

restrictedness but likewise applicable to programs over the same languages. We below

reproduce the concept of λ-restrictedness, called level-restrictedness here.

The idea underlying level-restrictedness is that the structure of a logic program Π

must be such that, for each rule r ∈ Π, the set of potentially applicable ground instances

of r is known in advance. This is the case if, for each variable V ∈ var (r), we ﬁnd an

atom A in the body of r with V ∈ var (A) (where var (A) is that set of variables oc-

curring in A) such that the potentially derivable ground instances of A are limited (see

below). In fact, with such an atom A at hand, the set of ground terms to which V needs

to be instantiated is known a priori, and no further ground terms need to be considered.

The sketched approach is justiﬁed by the ⊆-minimality of answer sets in the sense of

Π and Π are equivalent if they have the same answer sets.

剩余55页未读，继续阅读

DevilBox

粉丝: 35
资源: 35

使用指南：gringo, clasp, clingo与iclingo在Answer Set Programming中的应用

ASP非单调推理的各种求解器 以及程序范例

clingo-lessons:慢慢学习clingo，并编写笔记本以指导您完成逻辑程序（开发中）

python-clingox:with具有辅助功能的库可与clingo模块一起使用

Using gringo, clingo and iclingo

Gringo Nights

GrinGo-开源

iclingo的输入语言

gringo：MimbleWimble（Grin）的客户端

python-gringo:适用于Python的答案集编程

vim-minizinc:minizinc（CP）和gringo（ASP）源代码的语法突出显示

最新资源

ASP非单调推理的各种求解器以及程序范例