Gringo Understands Lukasiewicz's Theorem
Date: 20 May 2013
From: Vladimir Lifschitz
To: TAG
In 1941 Jan Lukasiewicz showed that disjunction is definable in terms of
other connectives in the three-valued propositional logic that is now
called HT, the logic of here-and-there. Specifically, he found that
the disjunction pVq is equivalent in HT to the formula
((p -> q) -> q) & ((q -> p) -> p). (L)
(It is clear that classically each of the two conjunctive terms is
equivalent to pVq. According to Lukasiewicz, if we include both
conjunctive terms then the equivalence will hold even in the weaker
logic HT.)
This theorem suggests that we may be able to rewrite a disjunctive rule
in an ASP program as a pair of nondisjunctive rules, corresponding to
the conjunctive terms of (L), if only we can find a way to represent
the implications p -> q, q -> p by expressions that are allowed in the
body of a rule.
Such expressions do exist in the input language of gringo, although this
fact is not widely known. They are called conditional literals. For any
two atoms A1, A2, the expression
A1 : A2
is a conditional literal ("A1 under the condition A2") that would be
written as the implication
A2 -> A1
in standard logical notation. (The term "conditional literal" is used by
the designers of gringo, rather that "conditional atom," because negation
as failure is actually allowed in front of each of the two atoms. But
this is not needed for our present purposes.)
When I learned about conditional literals a few months ago, one of my
first experiments with them was to rewrite (L) in the syntax of gringo:
p :- p:q.
q :- q:p.
I expected that the output of gringo could be processed then by clasp,
and that would give me the two stable models of the disjunctive program
p;q.
I suspected though that something might go wrong in the course of that
experiment, because clasp is not sufficiently powerful for processing
disjunctive programs. To deal with rules like p;q we need a disjunctive
solver, such as dlv, cmodels, or claspD.
Indeed, the experiment failed; gringo produced an error message:
ERROR: unstratified predicate in p:-p:q.
This is understandable, I thought; my two-rule program is semantically
correct (that is, strongly equivalent to the disjunctive rule p;q), but
gringo can't deal with it because of some implementation restriction.
Oh well.
And just recently I repeated that experiment with Version 4 of gringo,
released at the end of March. The result was quite different: no error
messages. The output that gringo-4 produced was not accepted by clasp
("clasp Read Error: Line 5, Unsupported rule type!"), but claspD gave me
the right answer:
claspD version 1.1.1. Reading...done
Answer: 1
q
Answer: 2
p
The same happened when I redirected the output of gringo-4 to cmodels:
cmodels version 3.81 Reading...done
Program is not tight.
Program is Disjunctive.
Program is HCF.
Calling SAT solver Minisat 2.0 beta ...
Answer: 1
Answer set: q
Answer: 2
Answer set: p
It seems that gringo-4 somehow turns rules with "unstratified predicates,"
which were formerly disallowed, into disjunctive rules. The process may be
related to the ideas of the 2007 paper by Pedro Cabalar and Paolo Ferraris
"Propositional theories are strongly equivalent to logic programs." But
this is only a guess, I don't know really. I hope Roland Kaminski, the
main architect of gringo-4, will clarify this.
To sum up, gringo-4, unlike gringo-3, understands Lukasiewicz's theorem
about the definability of disjunction in the logic of here-and-there.
I don't know if this fact will ever have any serious applications, but it
gives me tremendous intellectual satisfaction.
=======
Date: 21 May 2013
From: Torsten Schaub
To: Vladimir Lifschitz
I just wanted to add that "conditional literals" were invented by Tommi
Syrjanen and colleagues within lparse (there used in a more restricted
way). In modeling, their primary purpose is to provide finite yet
variable-length expressions, like conjunctions in bodies or disjunctions
in heads.
=======
Date: 21 May 2013
From: Roland Kaminski
To: TAG
Vladimir guessed correctly that I used the paper by Pedro Cabalar and Paolo
Ferraris to implement the translation (it's Lemma 1 in the paper). The only
difference is that gringo introduces some auxiliary atoms to be able to
apply the translation locally. I also added an option to inspect the
translations in a more readable format than the lparse-output. See the
example below.
Kind regards,
Roland
$ cat test.lp
p :- p:q.
q :- q:p.
$ gringo-4 -t --lparse-rewrite test.lp
#aux(1):-q.
#aux(2):-p.
#aux(1):-not #aux(2).
#aux(1)|#aux(2):-#not #not q.
p:-#aux(2).
#aux(0):-#aux(1).
q:-#aux(0).
#aux(4):-p.
#aux(5):-q.
#aux(4):-not #aux(5).
#aux(4)|#aux(5):-#not #not p.
q:-#aux(5).
#aux(3):-#aux(4).
p:-#aux(3).
PS: Currently, the translation introduces a few auxiliary symbols too much.
I should improve the implementation here.