Proof Search in Minimal Logic - Artificial Intelligence and Symbolic Computation - page 25

In this way we regain the property of a formula to have a unique head, and our
previous search procedure continues to work.
For the existential quantifier ∃ the problem is of a different nature. We chose

to introduce by means of axiom schemata. Then the problem is which of such

schemes to use in proof search, given a goal

∃

G and a set P of clauses. We might

proceed as follows.
List all prime, positive and negative existential subformulas of ,and

remove any formula from those lists which is of the form of another one 1 .For
every positive existential formula - say

P⇒G

∃xB

- add (the generalization of) the

existence introduction scheme

+
x,B

∃ : ∀x.B →∃xB

to P . Moreover, for every negative existential formula - say ∃xA - and every

(prime or existential) formula C in any of those two lists, exept the formula ∃xA

itself, add (the generalization of) the existence elimination scheme

∃ x,A,C : ∃xA → ( ∀x.A → C ) → C

to . Then start the search algorithm as described in section 4. The normal

form theorem for the natural deduction system of minimal logic with

P

∃ then

guarantees completeness.
However, experience has shown that this complete search procedure tends to
be trapped in too large a search space. Therefore in our actual implementation we
decided to only take instances of the existence elimination scheme with existential
conclusions.

Acknowledgements

I have benefitted from a presentation of Miller's [1] given by Ulrich Berger, in a
logic seminar in Munchen in June 1991.

References

1. Dale Miller. A logic programming language with lambda-abstraction, function vari-
ables and simple unification. Journal of Logic and Computation , 2(4):497-536, 1991.
2. Tobias Nipkow. Higher-order critical pairs. In R. Vemuri, editor, Proceedings of the
Sixth Annual IEEE Symposium on Logic in Computer Science , pages 342-349, Los
Alamitos, 1991. IEEE Computer Society Press.

1 To do this, for patterns the dual of the theory of “most general unifiers”, i.e., a
theory of “most special generalizations”, needs to be developed.