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:

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:

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

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:

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.

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

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^{i} z, n, s^{i} n).

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

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.

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

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