Polarities in Theorem Proving and Logic Programming

Kaustuv Chaudhuri
INRIA Futurs and École Polytechnique
France

Editor: Enrico Pontelli

Download: PDF

Andreoli famously observed [1] that the logical connectives divide precisely into two polarities determined by their inference rules in the sequent calculus. Connectives of the negative polarity, also called asynchronous, are such that their rules are invertible, i.e., their rules commute with every other inference rule. During proof-search such connectives may be decomposed at any time. Dually, connectives of the positive polarity, also called synchronous, have non-invertible rules: their rules commute only with those of other positive connectives. Andreoli discovered that it is complete for proof search to proceed in positive or negative phases that are maximal in the following sense: in the negative phase, negative rules are applied eagerly until no negative propositions remain; and a single proposition is selected for focus in the positive phase and positive rules are applied to it while maintaining focus until the focal proposition becomes negative.

A sequent with only positive connectives or atoms is called a neutral sequent. The only way to infer a neutral sequent is to decide on a proposition for focus. This focus persists upwards in the derivation until the phase transition to negative connectives, eventually producing a number of neutral sequents. Focusing is thus essentially a calculus of derived inference rules for neutral sequents. For example, in intuitionistic linear logic, the final goal sequent ( is the linear sequent arrow), corresponds to proving the two neutral sequents

and ,

which are the premisses of the final &-right and -right rules. The allowable derived rules are as follows, where R is some (positive) proposition.

The picture is completed once we have provided the treatment of the atomic propositions. Andreoli observed that it is sufficient for completeness to treat, arbitrarily, every atom as positive or negative, as long as duality is maintained across the sides of the sequent arrow. Furthermore, if a were a positive atom, then the only way to infer it under focus would be for the opposite side to match it precisely:

where  is a right-positive (resp. right-negative) atom and the square brackets indicate focus. In the above derived rules, for example, if a is positive on the right, then the derived rules for are:

and so on, where is instead replaced with a.

Is there ever a reason to pick one polarity over the other for the atoms? The answer is yes, and it is a matter of picking the desired semantics for proof-search. Precisely, the search for a positive proposition is “backward-chaining” or “goal-directed” because its foci operate on the conclusion of sequents which must be decomposed in such a way to match the hypotheses. Dually, a negative proposition is “forward-chaining” or “program-directed” as it decomposes a hypothesis to match the passive conclusion.

We illustrate this duality by means of an example on the Horn-fragment of the logic. Consider propositional Horn-logic where each Horn-clause where each p_i and q are atoms, is interpreted as a linear implication  Consider a left focus on this implication. If all the atoms are given negative polarity, then we obtain the following derived inference rule:

For unit clauses q, this is interpreted as an axiom of the form Thus, any derivation constructed from such axioms would have an empty collection of hypotheses except to have a number of copies of the Horn-clauses themselves, which may all be derelicted and contracted with the unrestricted copy of the Horn-clause of the logic program. We thus end up with just the rule:

which is the hyperresolution rule, familiar from theorem proving.

On the other hand, if we give every atom a positive polarity, then the derived rules (where we again delete the extra copy of the clause itself) is:

In particular, unit clauses q turn into the rule:

If we are to prove a given goal g then each R in the derived rules would have to be g, and the initial axiom would be of the form  Reading top-down, we see a strategy that starts with the desired goal in the context, and in each derived rule selects a literal from among the current goals in the context that is the head of a Horn-clause, and replaces it with the body of the clause. This is the famous SLD-resolution, familiar from top-down logic programming (such as in Prolog).

In the same reading of a proof (from the premisses down to the conclusion), we are thus able to obtain the two different semantics of Horn-clauses—forward chaining and backward chaining—as a direct consequence of the assignment of polarities to the atoms. It should be no surprise that in the opposite reading of the rules (from the conclusion to the premisses), we also observe (a dualised form of) SLD-resolution and hyperresolution. This observation extends (with some additional work) to first-order Horn-clauses also.

To slightly emphasize an easily missed consequence, we see that forward and backward reasoning can cohabit in the same general search strategy by careful assignment of polarity to the atoms. For an illuminating example, consider the computation of Fibonacci numbers by means of the following short collection of Horn-clauses.

fib(z, s z).        
fib(s z, s z).
fib(s s N, K), ¬fib(s M, I), ¬fib(M,J), ¬add(I,J,K).   
add(z,N,N).  
add(s M, N, s K), ¬add(M,N,K).

Suppose we assign both the fib and add predicates the negative polarity. The derived rule for the main clause of fib, thus, is:

And, for add, we observe the following derived rule for its main clause:

where M, N and K in the rule are meta-variables. If this rule were to be used in a saturation-based approach, applying the rules on premisses to construct new conclusions, then we would never saturate, as we would keep finding larger and larger proofs of add(sⁱ z, n, sⁱ n).

However, if we give add the positive polarity, then the rule for its second clause is:

In this case, the complexity of the terms in the conclusion actually decreases, so we can saturate. In this case, the derived rule for the main clause of fib is:

We then use the * rule above on the conclusion until the add predicate disappears from the context, after which we can apply the rule for fib again. We thus observe that not only does the correct assignment of polarities to the atoms give us saturation, but also that in each case the applicable rules are so constrained as to have only one possible path. In fact, for any goal sequent of the form there will be exactly i − 1 generated facts about fib. Sub-derivations will be shared as a matter of course. so the computational complexity will be linear in length of the answer substitution.

Note This article is a very brief summary of some results in [2, 3].

References

[1] Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992.
[2] Kaustuv Chaudhuri. The Focused Inverse Method for Linear Logic. PhD thesis, Carnegie Mellon University, December 2006. Also available as Technical Report CMU-CS-06-161.
[3] Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. In U Furbach and N Shankar, editors, Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR’06). Springer-Verlag LNCS 4130, 2006.