Answer Set Programming (asp)


Download 487 b.
Sana28.03.2017
Hajmi487 b.



Answer Set Programming (ASP)

  • Answer Set Programming (ASP)

    • Powerful and Elegant way of a Declarative Knowledge Representation and Nonmonotonic Reasoning in Normal Logic Programming (LP).
    • Stable Model (Answer Set) Semantics of logic programs, by Gelfond and Lifschitz (1988)
    • The Term ASP due to Lifschitz, as it was recognized as a new declarative paradigm.
    • Implementation in the late 90’s including Smodels and Lparse by Niemelä and Simons (1996), followed by DLV, Cmodels, ASSAT, NoMoRe …


Current implementations (of ASP solver) can handle only a class of ASP programs of “grounded version of a range-restricted function-free normal program” (Niemelä).

  • Current implementations (of ASP solver) can handle only a class of ASP programs of “grounded version of a range-restricted function-free normal program” (Niemelä).

    • Grounded
    • Range-restricted (finite domain of constants)
    • Function-Free (only variables)
    • Normal Program (with negation allowed)


Recent introduction of Coinductive Logic Programming (Co-LP) has been very promising to overcome many of these inherent limitations and restrictions of current ASP solvers.

  • Recent introduction of Coinductive Logic Programming (Co-LP) has been very promising to overcome many of these inherent limitations and restrictions of current ASP solvers.

  • Current work is an extension of our previous work for grounded (propositional) ASP solver:

    • Gupta, G., Bansal, A., Min, R., Simon, L., Mallya, A.: Coinductive Logic Programming and Its Applications. (Tutorial Paper). In: Proc. of ICLP07, pp. 27-44. (2007).


We achieve this novel and elegant ASP solver by co-LP with negation

  • We achieve this novel and elegant ASP solver by co-LP with negation

    • Coinductive SLDNF (co-SLDNF) resolution
  • Co-LP with co-SLDNF provides a viable and attractive alternative to

    • (a) current theoretical foundation and its implementation of current ASP solvers and
    • (b) current ASP language extending to first order logic with function symbols.


Answer Set Programming

  • Answer Set Programming

    • A-Prolog (Gelfond & Lifschitz), AnsProlog (Baral).
    • According to Niemelä,
    • Programs are some theories (of some formal system) with a semantics assigning a collection of sets (or models, referred to as answer sets of the program) to a theory.
    • A program devised to solve a problem using ASP
    • The solutions of the problem can be derived from the answer sets of the program.


The basic syntax of a ASP program:

  • The basic syntax of a ASP program:

  • Lo :- L1, … , Lm, not Lm+1, …, not Ln.

  • where Li is a literal where n  0 and n  m.

  • Lo must be in the answer set

  • if L1 through Lm are in the answer set and

  • if Lm+1 through Ln are not in the answer set.



Lo :- L1, … , Lm, not Lm+1, …, not Ln.

  • Lo :- L1, … , Lm, not Lm+1, …, not Ln.

  • If L0 =  (or null), then its head is null (meant to be false) to force its body to be false (a constraint rule or a headless-rule), written as follows.

  • :- L1, … , Lm, not Lm+1, …, not Ln.



The main difficulty in the execution of answer set programs is caused by the constraint rules, including headless rules, as well as rules of the form:

  • The main difficulty in the execution of answer set programs is caused by the constraint rules, including headless rules, as well as rules of the form:

  • Lo :- not Lo, L1, … , Lm, not Lm+1, …, not Ln.

  • Such rules are said to contain an odd-cycle in the predicate dependency graph.

  • A program is call-consistent if it contains no odd-cycle rules. A predicate ASP program is order-consistent if none of its rules when grounded produce an odd-cycle rule (that is, well-founded and acyclic).



Gelfond-Lifschitz Transformation (GLT)

  • Gelfond-Lifschitz Transformation (GLT)

    • To compute the (stable) models of a program.
    • Given a grounded program P and a candidate answer set CAS, a residual program R is obtained by applying the following transformation rules:
    • For all literals L  CAS,
      • To delete all rules in P which have “not L” in their body,
      • To delete all “L” from the bodies of the remaining rules.
      • The least fixpoint (say, F) of the residual program R is computed by repeating this process.
      • If F=CAS, then CAS is an answer set for P;
      • else repeat the process with R to be CAS.


Example 1 (Gelfond-Lifschitz Transformation).

  • Example 1 (Gelfond-Lifschitz Transformation).

  • Given a program P = { p :- not q. } and a candidate answer set CAS = { p }, since q is not in CAS, thus

  • p :- not q. => p.

  • This resulting reduct of { p } is same as CAS.

  • Thus { p } is an answer set of P.

  • Note that CAS can be { }, {p}, {q}, {p,q} or there is no Answer Set.



Example 2 (Gelfond-Lifschitz Transformation).

  • Example 2 (Gelfond-Lifschitz Transformation).

  • Given a program P = { p :- not q. q :- not p } and a candidate answer set CAS = { p },

  • Since q is not in CAS, thus

    • p :- not q. => p.
    • q :- not p. => 
  • This resulting reduct of { p } is { p }, which is same as CAS. Thus { p } is an answer set of P.



Example 3 (GLT). Given a program P = { p :- not p. } and a candidate answer set CAS1 = { p }, since p is in CAS1, thus

  • Example 3 (GLT). Given a program P = { p :- not p. } and a candidate answer set CAS1 = { p }, since p is in CAS1, thus

    • p :- not p. => 
  • Thus the resulting reduct of { p } is { }. Now CAS2 = { } and repeat GLT. Since p is not in CAS2,

    • p :- not p. => p.
  • Thus the resulting reduct of { } is { p }. Now CAS3 = { p } and repeat GLT to get CAS3 which is CAS1 and so on as CASi never converges. Thus no Answer Set.



Coinduction is the dual of induction.

  • Coinduction is the dual of induction.

  • Induction corresponds to well-founded structures that start from a basis which serves as the foundation for building more complex structures.



Induction is a mathematical technique for finitely reasoning about an infinite number of things.

  • Induction is a mathematical technique for finitely reasoning about an infinite number of things.

    • If there were only finitely many different things, than induction would not be needed.
    • Naturals: 0, 1, 2, …
    • The naïve “proof”
  • 3 components of inductive definition:

    • (1) Initiality, (2) iteration, (3) minimality
    • for example, a list is defined inductively
    • (1) [ ] – an empty list is a list (initiality)
    • (2) [ H | T ] – a list if T is a list and H is a list (iteration)
    • (3) nothing else is a list (minimality)


Coinduction is a mathematical technique for finitely reasoning about infinite things.

  • Coinduction is a mathematical technique for finitely reasoning about infinite things.

    • Mathematical dual of induction
    • If all things were finite, then coinduction would not be needed.
    • Perpetual programs,
    • Infinite strings: networks, model checking
  • 2 components of coinductive definition:

    • (1) iteration, (2) maximality
    • For example, a list is defined coinductively
    • (1) [ H | T ] is a list if T is a list and H is a list (iteration).
    • (2) The set of lists is the maximal set of such lists.


Duality provides a source of new mathematical tools that reflect the sophistication of tried and true techniques.

  • Duality provides a source of new mathematical tools that reflect the sophistication of tried and true techniques.



 (S) = { 0 }  { succ(x) | x  S }

  •  (S) = { 0 }  { succ(x) | x  S }

  • N = 

    • where  is least fixed-point.
  • aka “inductive definition”

    • Let N be the smallest set such that
      • 0  N
      • x  N implies x + 1  N
  • Induction corresponds to LFP interpretation.



(S) = { 0 }  { succ(x) | x  S }

  • (S) = { 0 }  { succ(x) | x  S }

  • unambiguously defines another set

  • N’ =  = N  {  }

    •  = succ( succ( succ( ... ) ) ) = succ(  ) =  + 1
    • where  is a greatest fixed-point
  • Coinduction corresponds to GFP interpretation.



model checking

  • model checking

  • bisimilarity proofs for process algebras

  • lazy evaluation

  • reasoning with infinite structures

  • perpetual processes

  • cyclic structures

  • operational semantics of “coinductive logic programming”



Traditional logic programming is unable to reason about infinite objects and/or properties.

  • Traditional logic programming is unable to reason about infinite objects and/or properties.

  • Computer Network example: perpetual binary streams (as traditional logic programming cannot handle).

  • For example, bit-stream of a bit-pattern

    • bit(0).
    • bit(1).
    • bitstream( [ H | T ] ) :- bit( H ), bitstream( T ).
    • |?- X = [ 0, 1, 1, 0 | X ], bitstream( X ).


Let node(A, L) be a constructor of a tree with root A and subtrees L, where A is an atom and L is a list of trees.

  • Let node(A, L) be a constructor of a tree with root A and subtrees L, where A is an atom and L is a list of trees.

  • A tree is rational if the cardinality of the set of all its subtrees is finite. An object such as a term, an atom, or a (proof or derivation) tree is said to be rational if it is modeled (or expressed) as a rational tree.

  • (2) A rational proof of a rational tree is its rational solved form computed by rational solved form algorithm.

  • (3) A coinductive proof of a rational (derivation) tree of program P is a rational solved form (tree-solution) of the rational (derivation) tree.



Coinductive hypothesis rule: (Simon et al. 2006) states that during execution,

  • Coinductive hypothesis rule: (Simon et al. 2006) states that during execution,

    • If the current resolvent contains a call C’ that unifies with an ancestor call C encountered earlier,
    • then the call C’ succeeds; the new resolvent is R’ where  = mgu(C, C’) and R’ is obtained by deleting C’ from R.
  • Ex. Program with C1: { p(X) :- p(f(X)). }, Query ?- p(X).

  • { p(X) } [C1 head]  { p(f(X)) } [C1 body, =mgu(p(X), p(f(X))) => X=f(X)]  { }.



With this rational feature, co-LP allows programmers to manipulate rational (finite and rationally infinite) structures in a decidable manner.

  • With this rational feature, co-LP allows programmers to manipulate rational (finite and rationally infinite) structures in a decidable manner.

  • To achieve this feature of the rationality, the unification has to be necessarily extended, to have “occur-check” removed.

  • Unification equations such as X=[1|X] are allowed in co-LP (that is, an infinite sequence or stream of 1, or a rational tree consisting of two nodes where the root node points to a node of 1 and to itself).

  • In fact, such equations will be used to represent infinite (regular) structures in a finite manner.



Co-SLD Resolution is very similar to SLD Resolution. Thus, given a call during execution of a logic program, the candidate clauses are tried one by one via backtracking.

  • Co-SLD Resolution is very similar to SLD Resolution. Thus, given a call during execution of a logic program, the candidate clauses are tried one by one via backtracking.

  • Under co-SLD resolution, apply the coinductive hypothesis rule to check if the current call will unify with any of the earlier calls.

  • If there is a cycle (or a circle) in the path of the execution, it will be detected by co-SLD and infinite traversal of this cycle stopped.



Design of “Coinductive Logic Programming” language extended with negation as failure (co-LP with co-SLDNF resolution).

  • Design of “Coinductive Logic Programming” language extended with negation as failure (co-LP with co-SLDNF resolution).

  • Designing a simple and efficient implementation technique to implement co-LP with co-SLDNF atop an existing Prolog engine.

  • Proof of the correctness (soundness and completeness) of co-SLDNF resolution.



4. Design of a Top-Down algorithm for goal-directed execution of propositional and predicate Answer-Set Programs.

  • 4. Design of a Top-Down algorithm for goal-directed execution of propositional and predicate Answer-Set Programs.

  • 5. Design of a simple and efficient implementation technique to implement the Top-Down propositional and predicate ASP atop an existing Prolog engine.

  • 6. Prototype implementation of co-ASP Solver



Co-LP with co-SLD was initially designed only for definite logic programs (that is, without negation).

  • Co-LP with co-SLD was initially designed only for definite logic programs (that is, without negation).

  • Thus the extension of co-LP to provide negation (that is, to have a negative literal) is somewhat natural and inevitable for research endeavor to extend the scope of co-LP to infer negative information and reason with negation.



Negation causes many problems in logic programming (e.g., nonmonotonicity).

  • Negation causes many problems in logic programming (e.g., nonmonotonicity).

  • For example, one can write programs whose meaning is hard to interpret (e.g., p :- not p. ) whose completion is inconsistent or execution is infinite).

  • However, there are many benefits and advantages to have negation in logic programming so that one may represent, reason and infer “what is not” in a Database or a Knowledgebase.



Two major inference rules dealing with negation are:

  • Two major inference rules dealing with negation are:

    • the closed world assumption (CWA) introduced
    • by Reiter, and
    • (2) the negation as failure introduced by Clark.
  • We choose negation as failure for co-LP, to be consistent with the semantics of SLDNF of the underlying Prolog engine.

  • We term the operational semantics of co-LP extended with negation as failure coinductive SLDNF resolution (co-SLDNF resolution).



Extending co SLD to co SLDNF,

  • Extending co SLD to co SLDNF,

    • the goal ?- nt(A). succeeds (or has a successful derivation) if A fails;
    • likewise, the goal ?- nt(A). fails (or has a failure derivation) if the goal ?- A. succeeds.
  • In co SLDNF (contrast to SLDNF),

    • any successful negated goals will be remembered as any negated goals can also succeed coinductively.


Co-SLDNF resolution extends co-SLD resolution with negation.

  • Co-SLDNF resolution extends co-SLD resolution with negation.

  • Essentially, it augments co-SLD with the negative coinductive hypothesis rule, stating:

  • If a negated call not(p) is encountered during resolution, and another call to not(p) has been seen before in the same computation,

  • then not(p) coinductively succeeds.



To implement co-SLDNF,

  • To implement co-SLDNF,

  • the set of positive and negative calls has to be maintained in

    • positive hypothesis table (denoted +) and
    • negative hypothesis table (denoted -) respectively.
  • Note that nt(A) below denotes coinductive “not” of A.

  • Note that  denotes an empty clause { }.



Definition (Co SLDNF Resolution):

  • Definition (Co SLDNF Resolution):

  • Suppose we are in the state (G, E, +, -)

  • where

  • G is a list of goals and

  • E is a set of substitutions (environment).

  • + is Positive Hypothesis Table, and

  • - is Negative Hypothesis Table.

  • Consider a subgoal A  G: .



(1) If A occurs in positive context (i.e., under even number of negations), and A’  + such that  = mgu(A,A’), then the next state is (G’, E, +, -), where G’ is obtained by replacing A with .

  • (1) If A occurs in positive context (i.e., under even number of negations), and A’  + such that  = mgu(A,A’), then the next state is (G’, E, +, -), where G’ is obtained by replacing A with .

  • If A occurs in negative context (i.e., under odd number of negations), and A’  - such that  = mgu(A,A’), then the next state is (G’, E, +, -), where G’ is obtained by A with false.



(3) If A occurs in positive context, and A’  - such that  = mgu(A,A’), then the next state is (G’, E, +, -), where G’ is obtained by replacing A with false.

  • (3) If A occurs in positive context, and A’  - such that  = mgu(A,A’), then the next state is (G’, E, +, -), where G’ is obtained by replacing A with false.

  • (4) If A occurs in negative context, and A’  + such that  = mgu(A,A’), then the next state is (G’, E, +, -), where G’ is obtained by replacing A with .



(5) If A occurs in positive context, then the next state is (G’, E’, {A}  +, -), where G’ is obtained by expanding A in G via normal call expansion with E’ as the new system of equations obtained.

  • (5) If A occurs in positive context, then the next state is (G’, E’, {A}  +, -), where G’ is obtained by expanding A in G via normal call expansion with E’ as the new system of equations obtained.

  • (6) If A occurs in negative context, then the next state is the (S1 or … or Sn) where Si is (G’i, E, +, {A}  -) for each clause Ci (where 1≤ i ≤ n) whose head atom is unifiable with A. Thus each G’i is obtained by expanding A in G via normal call expansion with Ci. Note that we require A to be ground, and therefore E is unchanged.



(7) If A occurs in positive or negative context and there are no matching clauses for A, and there is no A’  (+  -) such that A and A’ are unifiable, then the next state is (G’, E, +, {A}  -), where G’ is obtained by replacing A with false.

  • (7) If A occurs in positive or negative context and there are no matching clauses for A, and there is no A’  (+  -) such that A and A’ are unifiable, then the next state is (G’, E, +, {A}  -), where G’ is obtained by replacing A with false.

  • (8) (a) nt(…, false, …) reduces to , and

  • (b) nt(A, , B) reduces to nt(A, B) where A and B represent conjunction of subgoals.



Note

  • Note

  • (i) step (5) and (6) may be non-deterministic

  • (ii) the result of expanding a subgoal with a unit clause in step (5) and (6) is an empty clause (),

  • (iii) when an initial query goal reduces to an empty clause (), it denotes a success,

  • (iv) that “or” in step (6) is defined as follows:

  • (Si or (, E, +, -)) = ((, E, +, -) or Si) = (, E, +, -),

  • (Si or (false, E, +, -)) = ((false, E, +, -) or Si) = Si, and

  • ((false, E, +, -) or (false, E’, +’, -’)) = (false, E, +, -).



Co-SLDNF derivation of the goal G of program P is

  • Co-SLDNF derivation of the goal G of program P is

  • a sequence of co-SLDNF resolution steps with a selected subgoal A, consisting of

  • (1) a sequence (Gi, Ei, χi+, χi-) of state (i  0), of

    • (a) a sequence G0, G1, ... of goal,
    • (b) a sequence E0, E1, ... of mgu's (substitutions),
    • (c) a sequence χ0+, χ1+, ... of the positive hypothesis tables,
    • (d) a sequence χ0-, χ1-, ... of the negative hypothesis tables,
    • where (G0, E0, χ0+, χ0-) = (G, , , ) is the initial state, and


(2) for Definition (co-SLDNF resolution) (5-6), a sequence C1, C2, ... of variants of program clauses of P where Gi+1 is derived from Gi and Ci+1 using θi+1 where Ei+1 = Eiθi+1 and (χi+1+, χi+1-) as its resulting positive and negative hypothesis tables.

  • (2) for Definition (co-SLDNF resolution) (5-6), a sequence C1, C2, ... of variants of program clauses of P where Gi+1 is derived from Gi and Ci+1 using θi+1 where Ei+1 = Eiθi+1 and (χi+1+, χi+1-) as its resulting positive and negative hypothesis tables.

  • (3) If a co SLDNF derivation from G results in an empty clause of query , that is, the final state of (, Ei, χi+, χi-), then it is a successful co SLDNF derivation, and a derivation fails if a state is reached in the subgoal-list which is non-empty and no transitions are possible from this state.



C1,θ1

  • C1,θ1

  • (G0, E0, χ0+, χ0-) 

          • C2,θ2
  • (G1, E1, χ1+, χ1-) 

  • C3,θ3

  • (G2, E2, χ2+, χ2-)  ...

  • And a successful co-SLDNF derivation will result in: ({ }, En, χn+, χn-).



Consider the following program (NP1):

  • Consider the following program (NP1):

  • NP1: p :- nt(q).

  • q :- nt(p).

  • The query ?- nt(p) will generate the following transition sequence:

  • ({ nt(p) }, { }, { }, { }) by (6)

  •  ({ nt(nt(q)) }, { }, { }, {p}) by (5)

  •  ({ nt(nt(nt(p))) }, { }, {q}, {p}) by (2)

  • ({ }, { }, {q}, {p}) [success]



Note that the query ?- p will also succeed (p  nt(q)  nt(nt(p))  success)

  • Note that the query ?- p will also succeed (p  nt(q)  nt(nt(p))  success)

  • NP1 has two fixed points namely {p} and {q}.

  • The query ?- nt(p) is true in {q}, while the query ?- p is true in {p}. Thus, computing with greatest fix point semantics in presence of negation is always troublesome, since one has to be careful that given a query, different parts of the query are not computed w.r.t. different fixed points.

  • Thus, the query ?-p, nt(p) will never succeed if we are aware of the context (of a particular fixed point being used).





The -Automata consists of

  • The -Automata consists of

  • 4 states of {s0, s1, s2, s3} and

  • 5 events of {bootup, work, crash/off, shutdown, booterror, reboot}.

  • This example models the operation of a computer. The corresponding co-LP program code that models the automata is as follows:



state(s0,[s0|T]):-event(bootup), state(s1,T).

  • state(s0,[s0|T]):-event(bootup), state(s1,T).

  • state(s1,[s1|T]):-event(work), state(s1,T).

  • state(s1,[s1|T]):-event(crash/off), state(s2,T).

  • state(s2,[s2|T]):-event(shutdown), state(s0,T).

  • state(s0,[s0|T]):-event(booterror), state(s3,T).

  • state(s3,[s3|T]):-event(reboot), state(s0,T).

  • event(bootup).

  • event(work).

  • event(crash/off).

  • event(shutdown).

  • event(booterror).

  • event(reboot).



The query ?- state(S,T) may generate all possible paths, each ending with a cycle whereas the query ?- state(X,T), X=s0 will narrow the results to cycles starting from state s0 (** denotes a (rational) infinite list).

  • The query ?- state(S,T) may generate all possible paths, each ending with a cycle whereas the query ?- state(X,T), X=s0 will narrow the results to cycles starting from state s0 (** denotes a (rational) infinite list).

  • 1 X = s0, T = [s0, s1|**] ;

  • 2 X = s0, T = [s0, s1, s2|**] ;

  • 3 X = s0, T = [s0, s3|**]



The query ?- state(X,T), nt(state(s0,T)). shows cycles that do not start with s0.

  • The query ?- state(X,T), nt(state(s0,T)). shows cycles that do not start with s0.

  • 1 X = s1, T = [s1|**] ;

  • 2 X = s1, T = [s1, s2, s0|**] ;

  • 3 X = s1, T = [s1, s2, s0, s3|**] ;

  • 4 X = s2, T = [s2, s0, s1|**] ;

  • 5 X = s2, T = [s2, s0, s1|**] ;

  • 6 X = s2, T = [s2, s0, s3|**] ;

  • 7 X = s3, T = [s3, s0, s1|**] ;

  • 8 X = s3, T = [s3, s0, s1, s2|**] ;

  • 9 X = s3, T = [s3, s0|**]



The declarative semantics of co-SLDNF is based on the work of Fitting (Kripke-Kleene semantics with 3-valued logic, extended by Fages for stable model with completion of program).

  • The declarative semantics of co-SLDNF is based on the work of Fitting (Kripke-Kleene semantics with 3-valued logic, extended by Fages for stable model with completion of program).

  • The detailed account of co-SLDNF can be found in our Technical Report.



Let P be a general program over its rational Herbrand Universe HUR(P) and Herbrand Base HBR(P), given Herbrand Model HMR(P).

  • Let P be a general program over its rational Herbrand Universe HUR(P) and Herbrand Base HBR(P), given Herbrand Model HMR(P).

  • (1) (Soundness of co-SLDNF): (a) If A has a successful derivation in program P with co-SLDNF, then A is true in program P, i.e., A  HMR(P). (b) Similarly, if a grounded goal { nt(A) } has a successful derivation in program P, then nt(A) is true in program P, i.e., A  HBR(P)\HMR(P).



Let P be a general program over its rational Herbrand Universe HUR(P) and Herbrand Base HBR(P), given Herbrand Model HMR(P).

  • Let P be a general program over its rational Herbrand Universe HUR(P) and Herbrand Base HBR(P), given Herbrand Model HMR(P).

  • (2) (Completeness of co-SLDNF):

  • (a) If A  HMR(P), then A has a successful co-SLDNF derivation or an irrational derivation.

  • Further (b) if A  HBR(P)\HMR(P), then nt(A) has a successful co-SLDNF derivation or an irrational derivation.



Our current work on ASP is an extension of our previous work discussed in (Gutpa et al. 2007) for grounded (propositional) ASP solver to the predicate case.

  • Our current work on ASP is an extension of our previous work discussed in (Gutpa et al. 2007) for grounded (propositional) ASP solver to the predicate case.



Our approach possesses the following advantages:

  • Our approach possesses the following advantages:

  • First (1) it works with answer set programs containing first order predicates with no restrictions placed on them.

  • Second (2), it eliminates the preprocessing requirement of grounding, i.e., it directly executes the predicates. No grounding.



Third (3), it computes not only stable model semantics with least fixpoint (lfp) in the style of Gelfond-Lifschitz; but also it is capable of computing partial models (thus, providing a solution even for incomplete or inconsistent KnowledgeBase).

  • Third (3), it computes not only stable model semantics with least fixpoint (lfp) in the style of Gelfond-Lifschitz; but also it is capable of computing partial models (thus, providing a solution even for incomplete or inconsistent KnowledgeBase).



We term our strategy of solving answer set programming with co-LP as coinductive Answer Set Programming (co-ASP), and this ASP solver with co-LP as coinductive ASP Solver (co-ASP Solver).

  • We term our strategy of solving answer set programming with co-LP as coinductive Answer Set Programming (co-ASP), and this ASP solver with co-LP as coinductive ASP Solver (co-ASP Solver).



The co-ASP solver’s strategy is first to transform an ASP program into a coinductive ASP (co-ASP) program and use the following solution-strategy:

  • The co-ASP solver’s strategy is first to transform an ASP program into a coinductive ASP (co-ASP) program and use the following solution-strategy:

  • to execute the query goal using co-SLDNF resolution (this may yield a partial model),

  • (2) to eliminate loop-positive solution (e.g., p derived coinductively from rules such as { p :- p. }), and

  • (3) to perform an integrity check on the partial model generated, in order to account for the constraints.

  • (4) It constitutes a top-down, goal-directed and query-oriented paradigm for an ASP solver, a radically different alternative to current ASP solvers.



Given an odd-cycle rule of the form { p :- body, not p. }

  • Given an odd-cycle rule of the form { p :- body, not p. }

  • This integrity check, termed nmr_check, is crafted as follows:

  • If p is in the answer set, then this odd-cycle rule is to be discarded, else body must be false.

  • This can be synthesized as the condition: (p  not body) must hold true. The integrity check nmr_chk synthesizes this condition for all odd-cycle rules, and is appended to the query as a preprocessing step.

  • This solution strategy has been implemented and the results reported in our Technical Report (co-ASP).



Our current prototype implementation is a first attempt at a top-down predicate ASP solver, and thus is not as efficient as current optimized ASP solvers, SAT solvers, or Constraint Logic Programming in solving a practical problem.

  • Our current prototype implementation is a first attempt at a top-down predicate ASP solver, and thus is not as efficient as current optimized ASP solvers, SAT solvers, or Constraint Logic Programming in solving a practical problem.

  • However, we are confident that further research will result in much greater efficiency.

  • The main contribution of our current research is to demonstrate that top-down execution of predicate ASP is possible.



Most of the small ASP examples and their queries run very fast, usually under 0.0001 CPU seconds.

  • Most of the small ASP examples and their queries run very fast, usually under 0.0001 CPU seconds.

  • Our test environment is implemented on top of YAP Prolog running under Linux in a shared environment with dual core AMD Opteron Processor 275, with 2GHz with 8GB memory.



%% The original predicate ASP “move-win”

  • %% The original predicate ASP “move-win”

  • %% program move(a,b).

  • move(b,a). move(a,c). move(c,d). move(d,e). move(c,f). move(e,f).

  • win(X) :- move(X,Y), not win(Y).

  • %% query: ?- win(a).





Our first example is “move-win,” a program that computes the winning path in a simple game, tested successfully with various test queries. This is a predicate ASP program which is not call-consistent but order-consistent, and has two answer sets:

  • Our first example is “move-win,” a program that computes the winning path in a simple game, tested successfully with various test queries. This is a predicate ASP program which is not call-consistent but order-consistent, and has two answer sets:

  • { win(a), win(c), win(e) } and

  • { win(b), win(c), win(e) }.



The second example is the Schur number problem for NxB (for N numbers with B boxes).

  • The second example is the Schur number problem for NxB (for N numbers with B boxes).

  • First, Schur 12x5 is tested with query provided with a partial solution of length L (correct or incorrect).

  • That is, if L = 12, then co-ASP Solver will check the current query to be a solution. If L = 0, then co-ASP Solver will find a solution from scratch. The second case is the general Schur NxB problems with L=0 where N ranges from 10 to 18 with B=5.



box(1). box(2). box(3). box(4). box(5).

  • box(1). box(2). box(3). box(4). box(5).

  • num(1). num(2). num(3). num(4). num(5). num(6). num(7). num(8). num(9). num(10). num(11). num(12).

  • in(X,B) :- num(X), box(B), not not_in(X,B).

  • nt(in(X,B)) :- num(X[27]), box(B), not_in(X,B).

  • not_in(X,B) :- num(X), box(B), box(BB), B\==BB, in(X,BB).

  • nt(not_in(X,B)) :- num(X), box(B), in(X,B).

  • nmr_chk :- not nmr_chk1, not nmr_chk2.

  • nmr_chk1 :-num(X),box(B),in(X,B),(Y is X+X), num(Y),in(Y,B).

  • nmr_chk2 :-num(X),num(Y),box(B),in(X,B),in(Y,B),(Z is X+Y),num(Z),in(Z,B).

  • answer :- in(1,B1), in(2,B2), in(3,B3), in(4,B4), in(5,B5), in(6,B6), in(7,B7), in(8,B8), in(9,B9), in(10,B10), in(11,B11), in(12,B12).

  • %% Sample query: ?- answer, nmr_chk.





The following is an outline of the chapters and sections of the proposed dissertation.

  • The following is an outline of the chapters and sections of the proposed dissertation.

  • The two core chapters present the simple and efficient techniques to implement

    • co-LP with co-SLDNF and
    • co-ASP Solver for propositional and predicate ASP programs atop an existing Prolog engine.


Abstract

  • Abstract

  •  

  • 1. Introduction

  • 1.1 Co-Logic Programming

  • 1.2 Answer-Set Programming

  • 1.3 Dissertation Objective

  • 1.4 Dissertation Outline

  •  

  • 2. Background

  • 2.1 Induction and Coinduction

  • 2.2 Rational Tree and Proof

  • 2.3 Co-LP with co-SLD

  • 2.4 Answer Set Programming

  • 2.5 Conclusion

  •  



3. Coinductive Logic Programming with Negation

  • 3. Coinductive Logic Programming with Negation

  • 3.1 Extending co-LP with Negation: co-SLDNF

  • 3.2 Declarative and Operational Semantics

  • 3.3 Correctness Result

  • 3.4 Conclusion

  •  

  • 4. Answer Set Programming: Propositional

  • 4.1 Answer Set Programming: Propositional

  • 4.2 Propositional co-ASP Solver

  • 4.3 Correctness Result

  • 4.4 Examples

  • 4.5 Conclusion

  •  



5. Predicate Answer Set Programming

  • 5. Predicate Answer Set Programming

  • 5.1 Issues and Problems

  • 5.2 Predicate co-ASP Solver

  • 5.3 Correctness Result

  • 5.4 Examples

  • 5.5 Conclusion

  • 6. Conclusion

  • 6.1 Achievements and Contributions

  • 6.2 Future Research

  •  

  • Bibliography



(i) July, 2007: Design of “Coinductive Logic Programming” and “Co-Logic Programming” languages.

  • (i) July, 2007: Design of “Coinductive Logic Programming” and “Co-Logic Programming” languages.

  • (ii) September, 2007: Design of a simple & efficient implementation technique to implement the above mentioned languages atop an existing Prolog engine.

  • (iii) December, 2007: Design of a Top-Down algorithm for goal-directed execution of propositional ASP.



(iv) October, 2008: Theoretical Foundation of co-SLD and co-SLDNF

  • (iv) October, 2008: Theoretical Foundation of co-SLD and co-SLDNF

  • (v) November 2008: Design of a Top-Down algorithm for goal-directed execution of Predicate co-ASP Solver.

  • (vi) November 2008: Design of a simple & efficient implementation technique to implement the above mentioned co-ASP Solver atop an existing Prolog engine.



(vii) January 2009 (in progress): Prototype implementation of co-ASP Solver.

  • (vii) January 2009 (in progress): Prototype implementation of co-ASP Solver.

  • (viii) February 2009 (in progress): Dissertation writing and Defense.



We propose a comprehensive theory of co-LP with co-SLDNF resolution, implemented on top of YAP Prolog.

  • We propose a comprehensive theory of co-LP with co-SLDNF resolution, implemented on top of YAP Prolog.

  • In doing so, we have proposed a theoretical framework for declarative semantics of co-SLDNF adapted from the work of Fitting (Kripke-Kleene semantics with 3-valued logic) and extended by Fages for stable model with completion of program.

  • We have showed the correctness result of co-SLDNF resolution. This provides a concrete theoretical foundation to handle a cycle of predicates (positive or negative) in ASP.



We have designed and implemented the techniques and algorithms (co-ASP solver) to solve propositional and predicate ASP programs.

  • We have designed and implemented the techniques and algorithms (co-ASP solver) to solve propositional and predicate ASP programs.

  • We have showed the correctness result of co-ASP solver.

  • We note the limitation of our current approach in inconsistency-checking, restricted to the class of predicate ASP programs of call-consistent or order-consistent.



Our future work for co-LP may include

  • Our future work for co-LP may include

  • a language specification of co-LP with coinductive built-in predicates and system libraries,

  • its optimization and tuning,

  • its extension to concurrent and parallel processing, and

  • exploring co-LP to new domains of applications including modeling checking and verification.



Our future work for co-ASP Solver includes

  • Our future work for co-ASP Solver includes

  • a fully automated and optimized co-ASP Solver,

  • a utility to transform a ASP program into a co-ASP program,

  • a utility to check inconsistency of ASP program extending current restriction, and

  • extending a range of ASP applications with performance monitoring and benchmarking.



Gupta, G., Bansal, A., Min, R., Simon, L., Mallya, A.: Coinductive Logic Programming and Its Applications. (Tutorial Paper). In, Proc. of ICLP07, 27-44. (2007).

  • Gupta, G., Bansal, A., Min, R., Simon, L., Mallya, A.: Coinductive Logic Programming and Its Applications. (Tutorial Paper). In, Proc. of ICLP07, 27-44. (2007).

  • Min, R., Gupta, G.: Negation in Coinductive Logic Programming. Technical Report UTDCS34-08. Department of Computer Science. The University of Texas at Dallas (2008).

  • Min, R., Gupta, G.: Predicate Answer Set Programming with Coinduction. Technical Report (Draft). Department of Computer Science. The University of Texas at Dallas (2008).

  • Min, R., Gupta, G.: Negation in Coinductive Logic Programming. Submitted to ESOP'09.

  • Min, R., Gupta, G.: Toward Predicate Answer Set Programming with Coinduction. Submitted to AIAI’09.

  • Min, R., Gupta, G.: Coinductive Logic Programming with Negation with its Application to Boolean SAT. Submitted to FLAIRS’09.




Do'stlaringiz bilan baham:


Ma'lumotlar bazasi mualliflik huquqi bilan himoyalangan ©fayllar.org 2017
ma'muriyatiga murojaat qiling