Computing Stable Models of Normal Logic Programs Without Grounding

tags

s(ASP)

Notes

computing stable models of normal logic programs, i.e., logic programs extended with negation

NOTER_PAGE: (1 . 0.3933376040999359)

need not have a finite grounding, so traditional methods do not apply

NOTER_PAGE: (1 . 0.42280589365791155)

can be executed directly under the stable model semantics without requiring it to be grounded

NOTER_PAGE: (1 . 0.4606021780909673)

supports the use of terms as arguments

NOTER_PAGE: (1 . 0.5048046124279307)

negation as failure (NAF) has more interesting applications and has been widely researched

NOTER_PAGE: (1 . 0.6925048046124279)

logic programs with NAF can lead to multiple, incompatible models

NOTER_PAGE: (1 . 0.7399103139013452)

current methods compute the stable models of a program by first grounding the program

NOTER_PAGE: (2 . 0.19987187700192183)

only certain classes of programs are guaranteed to have a finite grounding

NOTER_PAGE: (2 . 0.32991672005124917)

each variable must be restricted to a finite domain

NOTER_PAGE: (2 . 0.4131966688020499)

often only interested in part of the model

NOTER_PAGE: (2 . 0.478539397821909)

adding negation can lead to (parts of) the program becoming inconsistent

NOTER_PAGE: (2 . 0.4939141575912876)

desirable to compute answers as long as these answers do not involve the inconsistent part of the program

NOTER_PAGE: (2 . 0.5445227418321589)

query-driven method that can apply the stable model semantics to a normal logic program containing arbitrary terms as well as negation

NOTER_PAGE: (2 . 0.7072389493914157)

well-founded semantics can be too weak for many applications, as it declares the truth value of many interesting atoms to be unknown. The stable model semantics is more expressive

NOTER_PAGE: (3 . 0.19987187700192183)

top-down, query-driven method that can execute normal logic programs with arbitrary predicates

NOTER_PAGE: (3 . 0.3779628443305573)

providing an operational semantics to nor- mal logic programs with predicates (or, Prolog with negation) under the sta- ble model semantics

NOTER_PAGE: (3 . 0.43625880845611786)

stable model semantics and answer set programming have been shown to support powerful reasoning techniques such as default reasoning, counter- factual reasoning, abductive reasoning, etc. These reasoning capabilities now become available within Prolog.

NOTER_PAGE: (3 . 0.5413196668802049)

only restrictions our method places upon programs are that operands of arithmetic operations must be ground, two negatively constrained variables (dis- cussed in Section 3.1.2) cannot be disunified with each other and left recursion cannot lead to success.

NOTER_PAGE: (3 . 0.6361306854580396)

we will refer to our method by the name given to its prototype implementation: s(ASP)

NOTER_PAGE: (3 . 0.7373478539397822)

normal logic program

NOTER_PAGE: (4 . 0.5477258167841127)

Under negation as failure (NAF), not p succeeds iff p fails.

NOTER_PAGE: (4 . 0.8616271620755925)

Under classical negation, -p and p cannot both be true, but it is possible for both to be false.

NOTER_PAGE: (5 . 0.1979500320307495)

classical negation can be used to define explicit rules for establishing falsehood.

NOTER_PAGE: (5 . 0.2645739910313901)

a call and its negation cannot both succeed.

NOTER_PAGE: (5 . 0.3068545803971813)

only positive literals may appear in the head of a rule

NOTER_PAGE: (5 . 0.3555413196668802)

The two key aspects of our propositional method are its handling of rules containing odd loops over negation and its use of coinduction.

NOTER_PAGE: (7 . 0.18129404228058935)

While the Herbrand universe may be finite, s(ASP) explicitly requires that its universe always be infinite

NOTER_PAGE: (10 . 0.3414477898782831)

The s(ASP) universe, US , is an infinite, proper superset of the Herbrand universe.

NOTER_PAGE: (10 . 0.43453355155482815)

Instead of the traditional states of bound and unbound, s(ASP) variables can be either bound or negatively constrained.

NOTER_PAGE: (10 . 0.8263933376040998)

values in a prohibited value list need not be ground, but must be at least partially bound.

NOTER_PAGE: (11 . 0.23126201153106982)

negatively constrained variable whose prohibited value list contains every element of D.

NOTER_PAGE: (11 . 0.4067905188981422)

It is impossible for a legal program to negatively constrain a variable against every element of the s(ASP) universe.

NOTER_PAGE: (11 . 0.5714285714285714)

A variable can never be empty with respect to the s(ASP) universe itself.

NOTER_PAGE: (11 . 0.6073030108904548)

The domain of a negatively constrained variable defined in terms of the s(ASP) universe will always be infinite.

NOTER_PAGE: (11 . 0.6201153106982703)

Given the query ?- p(X). the grounded program will always fail. However, execu- tion of the predicate program with s(ASP) will succeed, returning the solution { p(X), not d(X) (X \= 1) }.

NOTER_PAGE: (12 . 0.25240230621396537)

A legal program is a normal logic program, as defined in Definition 2, which satisfies the following restrictions: 1. Operands of arithmetic operations must be ground at the time they are exe- cuted. 2. Left recursion cannot lead to success. 3. A negatively constrained variable (see Section 3.1.2), cannot be disunified with or constrained against another negatively constrained variable.

NOTER_PAGE: (18 . 0.6399743754003844)