nmr_check.pl -- Detect OLON rules and construct nmr_check
Detect OLON rules and construct nmr_check.
Terminology:
- OLON: a loop with an odd number of default. negations in its
circular call dependency path.
- CHS: Coinductive Hypothesis Set, i.e., an atom that is true
due to coinduction, i.e. because it unifies with an ancestor.
- NMR check: non-monotonic reasoning check (from Computing Stable
Models of Normal Logic Programs Without Grounding by Kyle Marple
et al.
- author
- - Kyle Marple
- version
- - 20170127
- See also
- - An OLON is a loop with an odd number of default. negations in its
circular call dependency path, from "Layered Models Top-Down Querying of
Normal Logic Programs" by LM Pereira, PADL09.
- - "Galliwasp: A Goal-Directed Answer Set Solver" by Kyle Marple and
Gopal Gupta, LOPSTR 2012 for details on the NMR check
- license
- - BSD-3
- generate_nmr_check(+Module) is det
- Get the rules in the program containing odd loops and compute the
NMR check. After this step, headless rules are useless, so remove
them and add a fact for the negation of the dummy head (_false_0).
Call generate_nmr_check/0 instead of this.