## 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. ## 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 ## Thus the resulting reduct of { p } is { }. Now CAS2 = { } and repeat GLT. Since p is not in CAS2, ## 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 ## 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, - 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 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
## 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-) ## (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.4 Answer Set Programming ##
## 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 ## (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 ## 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:** |