How to flatten nested Prolog statements into a plain Horn clause

Question

I have a question about manipulating Prolog rules. My intent is to simplify a given rule with nested disjunction and conjunction expressions into a list of plain Horn-clause style rules. The reason why I do this is to convert a set of prolog code (https://nlp.jhu.edu/law/sara_v2/ dataset) to a rulebase for answer set programming (mainly for Potassco's Clingo).

For example,

answer(X) :- cond1(X),
             \+ (cond2(X), cond3(X)),
             (cond4(X)
              ; cond5(X), cond6(X)).

Should be splitted into a list of following rules:

answer(X) :- cond1(X), not cond2(X), cond4(X).
answer(X) :- cond1(X), not cond2(X), cond5(X), cond6(X).
answer(X) :- cond1(X), not cond3(X), cond4(X).
answer(X) :- cond1(X), not cond3(X), cond5(X), cond6(X).

I couldn't fine any relevant information based on keywords like 'simplifying prolog rules', 'converting prolog rules into Horn clauses', 'convert prolog into answer set programming', 'convert prolog into clingo format'.

Answer 1

Let's define some vocabulary: negation, conjunction, and disjunction are "control" terms; anything else is an "atomic" term:

controlterm(\+ _Term).
controlterm( (_A, _B) ).
controlterm( (_A ; _B) ).

atomicterm(Term) :-
    \+ controlterm(Term).

We want to relate a term Term to a "sufficient" term Sufficient; that is, a term such that the success of Sufficient is enough to make Term itself succeed.

We could start with something like this:

term_sufficient(\+ Term, \+ SuffTerm) :-
    term_sufficient(Term, SuffTerm).
term_sufficient( (A, B), (SuffA, SuffB) ) :-
    term_sufficient(A, SuffA),
    term_sufficient(B, SuffB).
term_sufficient( (A ; _B), SuffA) :-
    term_sufficient(A, SuffA).
term_sufficient( (_A ; B), SuffB) :-
    term_sufficient(B, SuffB).
term_sufficient(Term, Term) :-
    atomicterm(Term).

This is not bad, but it's incomplete because it doesn't look into negations:

?- term_sufficient( (cond1(X),
             \+ (cond2(X), cond3(X)),
             (cond4(X)
              ; cond5(X), cond6(X))) , Sufficient).
Sufficient =  (cond1(X), \+ (cond2(X), cond3(X)), cond4(X)) ;
Sufficient =  (cond1(X), \+ (cond2(X), cond3(X)), cond5(X), cond6(X)) ;
false.

To analyze negations, we must be aware that a negated conjunction behaves like a disjunction and vice versa (De Morgan's laws). So when we look at a term, we must interpret it according to whether it is inside a negation or not. For this we will track a "context" value, negated or not_negated. We must be able to switch contexts:

context_inverse(not_negated, negated).
context_inverse(negated, not_negated).

Now, the default behavior for finding "sufficient" terms will be to find them in a non-negated context:

term_sufficient(Term, Sufficient) :-
    term_context_sufficient(Term, not_negated, Sufficient).

and we need a definition like the above term_sufficient/2, but now with an extra context argument and separate rules for each kind of term. First, negation, which inverts the context before analyzing its operand:

term_context_sufficient(\+ Term, Context, SuffTerm) :-
    context_inverse(Context, InverseContext),
    term_context_sufficient(Term, InverseContext, SuffTerm).

Then, non-negated cases which are equivalent to the first try at defining term_sufficient/2:

term_context_sufficient( (A, B), not_negated, (SuffA, SuffB) ) :-
    term_context_sufficient(A, not_negated, SuffA),
    term_context_sufficient(B, not_negated, SuffB).
term_context_sufficient( (A ; _B), not_negated, SuffA) :-
    term_context_sufficient(A, not_negated, SuffA).
term_context_sufficient( (_A ; B), not_negated, SuffB) :-
    term_context_sufficient(B, not_negated, SuffB).
term_context_sufficient(Term, not_negated, Term) :-
    atomicterm(Term).

and then the corresponding negated cases, which are the duals of the rules above:

term_context_sufficient( (A ; B), negated, (SuffA, SuffB) ) :-
    term_context_sufficient(A, negated, SuffA),
    term_context_sufficient(B, negated, SuffB).
term_context_sufficient( (A, _B), negated, SuffA) :-
    term_context_sufficient(A, negated, SuffA).
term_context_sufficient( (_A, B), negated, SuffB) :-
    term_context_sufficient(B, negated, SuffB).
term_context_sufficient(Term, negated, \+ Term) :-
    atomicterm(Term).

Note how the rule for negation does not build a negated SuffTerm. Instead, the context argument passes information into the recursive analysis of subterms. Only when we encounter an atomic term in a negated context do we generate a negated atomic term.

Some tests:

?- term_sufficient( (cond1(X),
             \+ (cond2(X), cond3(X)),
             (cond4(X)
              ; cond5(X), cond6(X))) , Sufficient).
Sufficient =  (cond1(X), \+cond2(X), cond4(X)) ;
Sufficient =  (cond1(X), \+cond2(X), cond5(X), cond6(X)) ;
Sufficient =  (cond1(X), \+cond3(X), cond4(X)) ;
Sufficient =  (cond1(X), \+cond3(X), cond5(X), cond6(X)) ;
false.

?- term_sufficient( (a, \+ (b ; c), d), Sufficient).
Sufficient =  (a, (\+b, \+c), d) ;
false.

As you can see, a negated disjunction produces a parenthesized conjunction. This can be cleaned up in a separate post-processing step if needed.

If a predicate like answer is already defined in your Prolog program and you want to go directly from a clause head like answer(X) to the "sufficient" forms of clauses for that predicate, you can define this helper:

head_sufficientclause(Head, Head :- SufficientBody) :-
    clause(Head, Body),
    term_sufficient(Body, SufficientBody).

This grabs a matching clause from the database, translates its body to the "sufficient" form, then sticks the orignal head term back on. For example:

?- head_sufficientclause(answer(X), SufficientClause).
SufficientClause =  (answer(X):-cond1(X), \+cond2(X), cond4(X)) ;
SufficientClause =  (answer(X):-cond1(X), \+cond2(X), cond5(X), cond6(X)) ;
SufficientClause =  (answer(X):-cond1(X), \+cond3(X), cond4(X)) ;
SufficientClause =  (answer(X):-cond1(X), \+cond3(X), cond5(X), cond6(X)) ;
false.