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 cond