How to flatten nested Prolog statements into a plain Horn clause

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'.

Solution

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.