This paper develops a new formalism CDLP by combining ASP and constrained default logic to facilitate modeling questions with incomplete information, such that both Reiter's defaults and constraint defaults can be represented directly. After that, a method to split the CDLP programs is proposed by extending the notion of splitting sets to accommodate its property of constraint nonmonotonicity. Finally, we design a primary algorithm for solving the CDLP programs.
For example, an athlete plans to run both the marathon and the relay race in a game if possible.
It can be described by the following set 1 of default rules:
The default theory (1, ∅) has a consistent extension ℎ({ℎ, }). The following
ASP program Π1 is obtained from 1 by the translation in [
︂{ : ℎ
ℎ
,
: }︂
ℎ ← ¬ ∼
← ¬ ∼
ℎ.
.
Π1 has a unique answer set {ℎ, }. However, this method leads to the non-existence
of stable models if the inconsistency is not explicitly declared by strong negations [
However, the knowledge in 3 and 4 is beyond the original description of this problem, and it is hard for programmers to determine if the closed-world assumption is appropriate for the scenario. In summary, constraints in ASP programs are aimed at filtering models. Before filtering, the other rules must generate the desired models in this program, which may lead to extra work and unexpected results for programmers.
This paper introduces an extension of ASP, CDLP (Constrained Default Logic Programming), such that constrained defaults can be handled in logic programming. Specifically, a new unary operator C is added to ASP to represent defaults, such that C intuitively means is assumed to be consistent. By a new operator C of assumption, we can create new desired models with constraint rules while the rest constraints can still work as filters. The rest of this paper is organized as follows. Firstly, we introduce the syntax and semantics of CDLP in Section 3. Secondly, we investigate the splitting of CDLP programs in Section 4. We illustrate that the semantics of CDLP has the property of constraint nonmonotonicity. To accommodate this property, we extend the notion of splitting sets to CDLP programs and present the splitting theorem for CDLP. After that, we propose a primary algorithm for solving CDLP programs using the generate-and-test approach in Section 5. Then, we analyze the relationship between CDLP and constrained default logic in Section 6. Finally, the related works of belief and assume operators are surveyed in Section 7. 1By abuse of notation, in this paper, we let ¬ and ∼ denote negation as failure and strong negation, respectively. 1. 0 = 0 = , and 2. for ≥ 0
⊥} 3. ⟨, ⟩ = ⟨⋃︀∞=0 , ⋃︀∞ =0
⟩.
For a default rule : 1,...,
Constrained default logic (CDL) [
1, . . . , and are first-order sentences. is called the prerequisite, s the justifications, and the consequent. and can be obtained by
Let (, ) be a default theory, where is a set of defaults rules, a set of first-order sentences. The constrained extension of (, ) is a pair of set of sentences ⟨, ⟩, where • +1 = ℎ() ∪ { | : 1,..., ∈ ,
• +1 = ℎ() ∪ { ∧ 1 ∧ · · · ∧ |
∈ , ∪ { 1, . . . , , } ⊬ ⊥} : 1,..., ∈ , ∈ , ∪ { 1, . . . , , } ⊬ is the corresponding set containing all justifications that support . , 1, . . . , ∈ , then
∈ . As a result, is the set of consequences of reasoning,
The difference between CDL and Reiter’s DL is that CDL requires joint consistency, while it is not necessary for Reiter’s default theories. It means that in a classical default theory, two applied default rules to a consistent extension may have contradicted justifications, and the justification of an applied default rule should be consistent with the result of reasoning. In a word, in a constrained default theory, the set of formulas in , all justifications and consequents of applied rules to a constrained extension should be consistent, i.e.
∈ and a constrained extension ⟨, ⟩, if ∈ , and ∪ {, 1, . . . , |
: 1, . . . , is applied to (, )} ⊬ ⊥ is precisely the result we expected for this problem.
For example, consider the default theory (1, 1) in Section 1 as a constrained default theory. Since applying both default rules in 1 would cause inconsistency, (1, 1) has two CDL extensions, ⟨ ℎ({ℎ}), ℎ({ℎ})⟩ and ⟨ ℎ({}), ℎ({})⟩, which
An ASP program [
A constraint rule means that the literals in () can not be satisfied by a model at the same time. For example, “there is no penguin that is capable of flying” means an entity can not be a penguin while it can fly, which can be represented by the following rule.
← (), ().
There are three possible causes of inconsistency in an ASP program [
The constraints can be used to eliminate strong negations in an ASP program. For an ASP program Π, a literal ∼ can be eliminated by following steps: 1. replace all occurrences of ∼ with a new literal − , 2. adding the following constraint into program Π
An odd loop of negations [
, ¬, ¬, , .}.
A CDLP program is a finite collection of rules of the form 1| . . . | ← 1, . . . , , 1, . . . , . (3) where s are classical literals with or without strong negations, s are extended literals of the form or ¬, s are default literals of the form C or ¬C. The body of a rule , denoted by (), is defined as ⋃︀ ∪ ⋃︀ , while the head of , denoted by ℎ(), is defined as ⋃︀ . For a CDLP program Π, we use (Π) to denote the set of all default literals of the form C in the language of Π, and (Π) to denote the set of classical literals that occur in Π, i.e. ∈ (Π) iff. ∃ ∈ Π such that {, ¬, C, ¬C, C¬, ¬C¬} ∩ () ̸= ∅. The default literals provide an approach to express the constrained default theories in ASP programs.
Example 1 illustrates that default literals can be falsified by the inconsistency of both incoherence and constraints.
() ← (), C (). ∼ () ← ().
← (), ℎ().
Intuitively speaking, rules 2 and 3 are two different ways to represent the negation of default literals C () with strong negations and constraints, respectively. Consider an instance of and , rule 2 generates ∼ (), and will cause inconsistency if C () is true. Additionally, consider an instance of ℎ and , the constraint rule 3 forbids any model containing (); thus C () will cause inconsistency. As a result, both C () and C () are falsified, and both () and () are false in the models of this program.
The satisfiability of a CDLP program is defined as follows.
Definition 1 (Satisfiability) . A default interpretation of program Π is a pair of consistent literal sets ⟨, ⟩, where ⊆ ⊆ (Π). Let ⟨, ⟩ be a default interpretation of Π, • ⟨, ⟩ |= iff ∈ where is a literal; • ⟨, ⟩ |= ¬ iff ⊭ where is an extended literal; • ⟨, ⟩ |= C iff ∈ ; • ⟨, ⟩ |= C¬ iff ⊭ ; • ⟨, ⟩ |= ¬C iff ⟨, ⟩ ⊭ C; • ⟨, ⟩ |= iff ∃ ∈ ℎ() : ⟨, ⟩ |= or ∃ ∈ () : ⟨, ⟩ ⊭ , where is a rule in Π, is an extended literal in the head of , is an extended literal or default literal; • ⟨, ⟩ |= Π iff ∀ ∈ Π : ⟨, ⟩ |= .
A default interpretation of a CDLP program contains two parts and , where is the consequence of reasoning, and contains all the assumptions that is based on. (1) (2) (3) (1) (2)
← ← .
C.
The assumption of will not cause inconsistency because it does not mean is proved. Thus a model of Π2 that satisfies C does not necessarily satisfy . A default interpretation of Π2 is = ⟨{}, {, }⟩, and |= C while ⊭ .
C C¬ ¬C ¬C¬ ⟨, ⟩ |= remove remove replace with ¬ replace with ⟨, ⟩ ⊭ delete the rule delete the rule delete the rule delete the rule
With the definition of satisfiability, we can define the semantics of ASP programs with defaults as follows.
Definition 2 (Default Reduct). Let Π be an ASP program with defaults, = ⟨, ⟩ be a default interpretation of Π. The default reduct of Π w.r.t ⟨, ⟩ is a pair of ASP programs Π = ⟨Π , Π ⟩, where Π is obtained from Π by eliminating all default literals as Table 1, and Π is obtained from Π by adding fact rules for every literal in , i.e., Π = Π ∪ {.| ∈ }.
For a default interpretation = ⟨, ⟩ of Π, Π and Π are two ASP programs without defaults, while Π eliminates all default literals according to the assumptions in . As a result, a consequence ⟨, ⟩ of program Π, or a default model, should be a default interpretation that is concluded by Π , and Π is satisfiable.
Definition 3 (Default Models). Consider a CDLP program Π, a default interpretation = ⟨, ⟩, Φ(, Π) be a set of default literals of the form C in Π that is satisfied by , i.e., Φ(, Π) = {C|C ∈ (Π), |= C}. ⟨, ⟩ is a default model of Π iff. it satisfies the following conditions.
The first condition of Definition 3 means is a minimal model w.r.t the assumption . The second condition means is consistent with Π . Additionally, the third and fourth conditions mean all literals in ∖ are assumptions with corresponding default literals, and contains as many assumptions as possible.
Example 3 (Continue Example 2). For the program Π2, = ⟨ = {}, = {, }⟩ is a default interpretation. The default reduct Π is a pair ⟨Π , Π ⟩, where Π is ← .
. and Π is ← .
.
. 1. is an answer set of Π , 2. Π is satisfiable, 3. = ∪ {|C ∈ Φ(, Π)}, 4. ∄⟨ ′, ′⟩ ∈ (Π) s.t. Φ(, Π) ⊊ default models of Π.
Φ( ′, Π), where (Π) denotes the set of all Apparently, is an answer set of Π , and Π is satisfiable. Meanwhile, ∖ contains the only literal in Φ(, Π2) and Π2, which means contains maximal assumptions. Therefore, is a default model of Π2.
By the fourth condition in Definition 3, CDLP also provides a method to distinguish the negation of assumption (¬C) and the assumption of negation (C¬).
←
C¬. Π3 represents an assumption of negation, which means is true if ¬ is consistent. Obviously, Π3 has a unique default model ⟨{}, {}⟩. Meanwhile, by Π4, is true if is not consistent, which is not justified by any fact or rule. Therefore, ⟨∅, {}⟩ is the only default model of Π4.
As a result, we can describe the athlete’s problem in Section 1 as follows.
Example 5 (Athlete’s Dilemma). The athlete’s dilemma in Section 1 can be described with a
ℎ ← ← ←
Cℎ.
C.
ℎ, . 1 = ⟨{ℎ}, {ℎ}⟩ and 2 = ⟨{}, {}⟩.
The constraint monotonicity is an important property for ASP logic programs. A semantics satisfies constraint monotonicity if, for any ASP program Π and a constraint rule , there does not exist a stable model of Π ∪ {} such that is not a stable model of Π. However, CDLP obviously does not satisfy this property.
Corollary 1 (Constraint Nonmonotonicity). The semantics of CDLP is not constraint monotonic.
This corollary can be proved by the following example.
Example 6. Consider following program Π6: { ← C.} and a constraint rule : ← . Π6 has a unique default model = ⟨{}, {, }⟩, while Π6 ∪ {} has a unique default model ′ = ⟨∅, ∅⟩. (1) (2) (3)
An observation of Example 6 is that the constraint rule does not entail ′ ⊭ C directly. It rejects the default model produced by Π6, and brings out a new guess of default literals that C is not satisfied. It means that whether a default literal C is satisfied is not only affected by the rules depends, and also by the rules depends directly or indirectly.
In a standard ASP program Π, constraint rules are always in the top part (Π) with regard to a splitting set , because ℎ() of a constraint rule is always empty. Since the semantics of CDLP does not satisfy constraint monotonicity, the literals in constraint rules should be calculated ifrst. We can define the splitting set of CDLP by modifying the splitting set of ASP such that all constraint rules belong in the bottom part.
Definition 4 (Strong Splitting Set). Let Π be a CDLP program without odd loops. A splitting set of Π is a set ∈ (Π) such that for every rule ∈ Π, if ℎ() ∪ ̸= ∅, or ℎ() = ∅, then () ∈ . The set of rules ∈ Π such that () ⊆ is called the bottom of Π w.r.t. , and is denoted by (Π). The set of rules Π∖ (Π) is called the top of Π w.r.t , and is denoted by (Π).
←
C. ← ← .
C.
(1) (2) (3) Let = {, } be a splitting set of Π7. Thus we have (Π7) = {1, 2}, and (Π7) = {3}.
Let be a default model of (Π). For every rule , if for every extended literal (or default literal) in (), () ⊆ → |= , then we say is not falsified by . We can obtain a rule ′ from every ∈ (Π) by following steps if is not falsified: • ℎ(′) = ℎ(), and • if there is an extended literal or default literal that () ∈ , then remove from (′).
We denote the set of obtained rules by (Π∖ (Π), ).
Definition 5 (Solution). Let Π be a CDLP program without odd loops, be a splitting set of Π. A solution to Π with regard to is a pair ⟨, ⟩ such that 1. is a default model of (Π), and 2. is a default model of (Π∖ (Π), ), and 3. for = ⟨, ⟩ and = ⟨, ⟩, ∪ and ∪ are consistent respectively. Theorem 1 (Strong Splitting Theorem). Let Π be a CDLP program without odd loops, be a strong splitting set of Π. ⟨, ⟩ is a default model of Π, if and only if there exists a solution ⟨⟨, ⟩, ⟨, ⟩⟩ w.r.t such that = ∪ and = ∪ .
← ← ¬
C.
, . |. ← ¬ ←
.
C. ← ← .
, ¬. ← ←
C.
C.
← ← .
C. Π9 should have two splitting sets {} and {}.
Further observation shows that if a literal belongs in the bottom part (Π), literals in a rule that depends on C should also belong in (Π).
Although a strong splitting set can be used to split a CDLP program, Definition 4 is too strong for many conditions. For example, for CDLP programs with odd loops, a strong splitting set can not split these programs correctly.
If we extend Definition 4 to CDLP programs with odd loops, = {} was a strong splitting set of Π8. Therefore, there was a solution ⟨, ⟩ of Π8, where = ⟨{}, {, }⟩ and = ⟨∅, ∅⟩. However, 2 in this program is a rule with an odd loop, which implies that will lead to a contradiction, and C should not be satisfied by any default models. As a result, = ⟨∅, ∅⟩ is the unique default model of Π8. Apparently, ⟨, ⟩ is not a solution corresponding to .
On the other hand, if a program consists of two sets Π′ and Π′′ of rules with disjoint literals, then Π′ and Π′′ can both contain constraint rules.
Example 9. Consider following program Π9: (1) (2) (1) (2) (3) (4) (5)
Figure 1 is the support graph of Π10. In Figure 1, both 4 and 5 are used to represent inconsistency. It shows that 4 is indirectly dependent on C. As a result, every literal that depends on should also belong in . Thus Π10 has a splitting set = {, , , }, and (Π10) = {1, 2, 3, 4}.
Definition 6 (Splitting Set). Let Π be a program, and − be two sets of literals in (Π). is a splitting set if for every rule ∈ Π, • if ℎ() ∩ ̸= ∅, then () ∈ , and
U + r1 p u
U −
• for every literal ∈ (Π), if ∈ , then there exists a set − of literal such that – ∈ − , and – if (()) ∩ − ̸= ∅, then () ⊂ − , and – − ⊆ .
According to the denfiition above, the splitting set of Π10 in Example 10 is + ∪ − in Figure 1, where + contains all literals in 1, and − contains all literals in 3 and 4. Theorem 2 (Splitting Theorem). Let Π be a CDLP program, a splitting set of Π. ⟨, ⟩ is a default model of Π, if and only if there exists a solution ⟨⟨, ⟩, ⟨, ⟩⟩ w.r.t such that = ∪ and = ∪ .
We propose a primary algorithm for solving CDLP programs based on the idea of generate-andtest.
From Example 3, we can find that the Π in a default reduct is only affected by in the interpretation = ⟨, ⟩, or more specifically, by Φ(, Π). Therefore, for a guess about which default literals are satisfied, we can build a collection of default interpretations satisfying Condition 1 to 3 in Definition 3, which is called candidate default models and denoted by (Π).
For a guess of a CDLP program Π, where ⊆ (Π), the candidate default models w.r.t is obtained by following steps: 1. generate Π according to Table 2, which is a variation of Table 1. 2. obtain the parts by solving the ASP program Π . 3. for a possible , obtain by union and the literals in and check if the part satisfies Π⟨, ⟩.
Once we calculated all candidate default models of a program Π, we can get the default models of Π by comparing the Φ(, Π) of these candidate default models. Since the guesses contain all default literals in function Φ, we can also compare the subset relation between guesses. Additionally, by sorting the guess sequence, we can make sure that whenever we are testing guess , the super sets of are already tested. Thus we only need to check whether there is a default model with a tested guess , where ⊂ .
The algorithm above is formally described in Algorithm 1.
Algorithm 1: solving a CDLP program
Input: Π, a CDLP program
Output: DM, the set of all default models of Π 1 DM ← ∅ // obtain sorted consistent guesses s.t.
∀, : ( ⊃ ) → ( < ) 2 Guess = GuessDefault(Π) 3 foreach ∈ Guess do 5 if ∄⟨Cal′c,ula′⟩te∈ΠDMacsc.to. rdi⊂ ng to Table 2 4 Φ( ′, Π) then 6 7 8
Solve (Π ) with existing ASP solvers foreach ∈ (Π ) do ← ∪ {|C ∈ } // check if ⟨, ⟩ is a default model Generate Π⟨, ⟩ if Satisfiable(Π⟨, ⟩) then
DM ←
DM ∪{⟨, ⟩} 9 10 11 Theorem 3 (Soundness and Completeness of Algorithm 1). Let a CDLP program Π be the input of Algorithm 1, and is the set of default interpretations output by Algorithm 1. A default interpretation is a default model of Π, if and only if ∈ .
For a CDLP program Π and a guess ∈ (Π), the calculation of default reduct Π is
polynomial, while the calculation of and Π is as difficult as solving an ASP program, which
is in Σ2 [
We can establish a correspondence between CDLP programs and constrained default theories. Let Π be a CDLP program without disjunction heads or negation as failure, then its corresponding CDL theory (Π) = ( , ) is obtained by following steps. For a rule in a program Π with following form:
0 ← 1, . . . , , C+1, . . . , C. 1. if 0 is a literal and () is not empty, its corresponding default () ∈ is (4) (5) (6) 2. otherwise, its corresponding formula () ∈ is 1 ∧ · · · ∧ : +1, 0 1 ∧ · · · ∧
⊃ 0 where 0 may be a literal or ⊥.
Theorem 4. Let Π be a CDLP program without disjunction and negation as failure, and (Π) the corresponding constrained default theory.
(Π). • if ⟨, ⟩ is a default model of Π, then ⟨ ℎ(), ℎ( )⟩ is a constrained extension of • If ⟨, ⟩ is an extension of (Π) with maximal(w.r.t. inclusion) justifications and satisfiable, then there is a default model ⟨, ⟩ of Π such that = ℎ() and ℎ( ). Π is
←
C. ←
C. ← , . ︂( = ︂{ : : }︂ , , = { ∧ ⊃ ⊥} ︂) 2 = ⟨ ℎ({}), ℎ({, })⟩.
Apparently, the program Π11 has two default models ⟨{}, {, }⟩ and ⟨{}, {, }⟩, while
the default theory (Π11) has two constrained extensions, 1 = ⟨ ℎ({}), ℎ({, })⟩ and
There are many existing works on the consistency operators in logic programs. Logic GK of
minimal knowledge and justified assumption [
Some logic paradigms that support the joint consistency of assumptions, such as deontic logic
and DL-semantics for answer sets. Deontic logic [
This paper proposes a new ASP paradigm CDLP concerning the constraint default logic defined on a popular idea of joint consistency in commonsense reasoning. Unlike the existing default logic variants defined in the classical first-order logic, negation as failure is allowed in CDLP. It thus provides a more powerful tool to deal with incomplete information. The splitting theorem and an algorithm to solve the CDLP program are given.
In the future, we plan to investigate more properties of CDLP, for example, the Kripke semantics for CDLP. Moreover, we also plan to develop a parallel algorithm for solving CDLP programs based on the splitting set and the primary algorithm presented in this paper and develop a parallel solver. In addition, we plan to model some real-world applications with CDLP and solve these problems with the solver.