NonH: a Preprocessor for Generating non-Herbrand Stable Models

Description

NonH is a Python-based script that can be used to generate non-Herbrand stable models in the sense of the paper

Paolo Ferraris, Joohyung Lee, and Vladimir Lifschitz, Stable Models and Circumscription.

It turns a logic program P in the input language of Gringo into a program Q in the language of Gringo such that the Herbrand stable models of Q correspond to the stable models of P that satisfy the domain closure assumption but may violate the unique name assumption. The underlying theory is described in the paper

Vladimir Lifschitz, Karl Pichotta, and Fangkai Yang, Relational Theories with Null Values and Non-Herbrand Stable Models.

Current version of NonH is ver.0.1 The software is maintained by Fangkai Yang. Any bug reports should be sent to fkyang@cs.utexas.edu.

Download

The program can be downloaded from here. It currently runs correctly on Python 2.6.5.

Usage

The format of the command line is

$ nonH.py <filename> [ <option> <list of constants> ]

where:

<filename> is an input file containing a logic program in the language of Gringo
<option> is either -una or -no-una

<list of constants> is a list of object constants separated by blanks

NonH.py reads input from a file and outputs to stdout, and can be redirected to Gringo and Cmodels/Clasp/ClaspD to generate answer sets. The option -una instructs the program to conjoin its output with the unique name axioms for all pairs of distinct constants from the given list. The option -no-una instructs the program to conjoin its output with the unique name axioms for all pairs of distinct constants such that at least one of them does not belong to the given list.

Examples

Example 1. Consider the one-rule program "disjunction.lp":

p(a) | p(b).

We can use NonH.py for preprocessing and use Gringo+ClaspD, or Gringo+Cmodels, to generate its stable models, including those that do not satisfy the unique name assumption. In one of them, a is different from b, P(a) is true, and P(b) is false. In another, a is different from b, P(a) is false, and P(b) is true. In the third, a equals b and both P(a) and P(b) are true.

$ nonH.py disjunction.lp | gringo | claspd 0

Answer: 1
eq(b,b) eq(a,a) p(b)
Answer: 2
eq(b,b) eq(a,a) p(a)
Answer: 3
eq(b,b) eq(a,a) eq(b,a) eq(a,b) p(a) p(b)

Example 2. Consider the program "db.lp":

part(p1;p2;p3).
supplier(acme;foo;omega).
supplies(acme,p1;;foo,p2;;omega,p3).
subpart(p1,p2).

:- omega==p1.
:- omega==p2.
:- omega==p3.
　

It describes a relational database with the null value Omega -- a supplier that may be identical to Acme or to Foo, or can be different from both of them. There are three stable models, corresponding to these three possibilities.

$ nonH.py db.lp -no-una omega| gringo |clasp 0

Answer: 1
part(p1) part(p3) part(p2) supplier(acme) supplier(omega) supplier(foo) supplies(omega,p3) supplies(foo,p2) supplies(acme,p1) subpart(p1,p2) eq(omega,omega) eq(foo,foo) eq(acme,acme) eq(p3,p3) eq(p2,p2) eq(p1,p1) eq(omega,foo) eq(foo,omega) supplies(omega,p2) supplies(foo,p3)
Answer: 2
part(p1) part(p3) part(p2) supplier(acme) supplier(omega) supplier(foo) supplies(omega,p3) supplies(foo,p2) supplies(acme,p1) subpart(p1,p2) eq(omega,omega) eq(foo,foo) eq(acme,acme) eq(p3,p3) eq(p2,p2) eq(p1,p1)
Answer: 3
part(p1) part(p3) part(p2) supplier(acme) supplier(omega) supplier(foo) supplies(omega,p3) supplies(foo,p2) supplies(acme,p1) subpart(p1,p2) eq(omega,omega) eq(foo,foo) eq(acme,acme) eq(p3,p3) eq(p2,p2) eq(p1,p1) eq(omega,acme) eq(acme,omega) supplies(acme,p3) supplies(omega,p1)

Example 3. Consider the program written in F2LP syntax

(p(a) & p(b))| (p(c) & p(d)).
　

nonH can be used after F2LP and before Gringo to generate its non-Herbrand models:

$ f2lp formula | nonH.py | gringo | claspd 0

Answer: 1
eq(b,b) eq(d,d) eq(a,a) eq(c,c) p(a) p(b)
Answer: 2
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(d,c) eq(c,d) p(a) p(b)
Answer: 3
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,a) eq(a,b) p(a) p(b)
Answer: 4
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,a) eq(d,c) eq(a,b) eq(c,d) p(a) p(b)
Answer: 5
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(d,a) eq(a,d) p(a) p(d) p(b)
Answer: 6
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,d) eq(d,b) p(a) p(d) p(b)
Answer: 7
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,d) eq(b,a) eq(d,b) eq(d,a) eq(a,b) eq(a,d) p(a) p(d) p(b)
Answer: 8
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(a,c) eq(c,a) p(c) p(a) p(b)
Answer: 9
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,c) eq(c,b) p(c) p(a) p(b)
Answer: 10
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,a) eq(b,c) eq(a,b) eq(a,c) eq(c,b) eq(c,a) p(c) p(a) p(b)
Answer: 11
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,c) eq(c,b) p(c) p(d) p(b)
Answer: 12
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,c) eq(d,a) eq(a,d) eq(c,b) p(c) p(a) p(d) p(b)
Answer: 13
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,d) eq(b,c) eq(d,b) eq(d,c) eq(c,b) eq(c,d) p(c) p(d) p(b)
Answer: 14
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,d) eq(b,a) eq(b,c) eq(d,b) eq(d,a) eq(d,c) eq(a,b) eq(a,d) eq(a,c) eq(c,b) eq(c,d) eq(c,a) p(c) p(a) p(d) p(b)
Answer: 15
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(d,c) eq(c,d) p(c) p(d)
Answer: 16
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(d,a) eq(d,c) eq(a,d) eq(a,c) eq(c,d) eq(c,a) p(c) p(a) p(d)
Answer: 17
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,d) eq(d,b) eq(a,c) eq(c,a) p(c) p(a) p(d) p(b)
Answer: 18
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,d) eq(d,b) p(c) p(d) p(b)
Answer: 19
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(d,a) eq(a,d) p(c) p(a) p(d)
Answer: 20
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(a,c) eq(c,a) p(c) p(a) p(d)
Answer: 21
eq(b,b) eq(d,d) eq(a,a) eq(c,c) p(c) p(d)
Answer: 22
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,a) eq(d,c) eq(a,b) eq(c,d) p(c) p(d)
Answer: 23
eq(b,b) eq(d,d) eq(a,a) eq(c,c) eq(b,a) eq(a,b) p(c) p(d)