[Prev][Next][Index][Thread]
Herbrand Methods in Linear Logic
Date: Wed, 29 Jan 92 11:54:04 +0100
To: linear@cs.stanford.edu
A result in classical logic which has been largerly exploited
in logic programming is the Herbrand theorem.
Such a result allows the use of unification rather than of blind
instantiation when proofs are built up, thereby reducing
non-determinism and complexity in proof-search.
It would be nice to dispose of similar tools when searching
for linear proofs; unfortunately not every linear formula can
be put in prenex form, so that it does not make much sense
trying to get exactly this kind of theorem in linear logic.
However, the idea underlying the proof of
the classical theorem, namely to express universally
quantified variables as Herbrand functions of the
existential ones, may be exploited also
in the linear context; indeed, I propose a new proof-system
LLH for linear logic based on this idea. LLH is equivalent
to standard linear sequent calculus LL. The result is
perhaps not surprising, but it can contribute, I think, to the
work in the area of linear logic programming.
Serenella Cerrito
L.R.I., bat 490,
Universite` Paris XI
91405 Orsay Cedex
FRANCE
serena@lri.lri.fr
----------------------------------------
The proof-system LLH acts on formulae and terms which contain
special variables W1,W2,.... called "witness" variables.
Notation: here we write ~A to mean: linear negation of A,
V to indicate the existential quantifier, /\ to indicate
the universal quantifier, Gamma to indicate a context in
a right-handed sequent.
The identity group of LLH differs from LL just because the
identity axioms are replaced by the following identity rules :
W1=t1,...,Wn=tn
--------------------------
|- A,~A'
where the premise is such that W1,...,Wn
are among the witness variables in A, A' and the set of
equations W1=t1,...,Wn=tn represents a substitution
for these variables which is the most general unifier
of A and A'.
The only other rules which change in LLH w.r.t. to LL
are the quantifiers rules, which now become :
|- Gamma, A(x/Wi)
--------------------------------(exists)
|- Gamma, VxA(x)
where Wi is a fresh witness variable;
|- Gamma, A(x/f(W1,...,Wn))
------------------------------------(forall)
|- Gamma, /\xA(x)
where W1,..,Wn are all the witness variables in the
conclusion and f is a fresh Herbrand function.
Proofs in LLH are defined in such a way that the
substitutions associated to the leaves of the several
branches (let's call them ``partial answers")
must be compatible. Hence one can define the
notion of "answer" for the witness variables provided
by a LLH-proof.
Not only LL et LLH are equivalent, but there is a
strict correspondence between proofs in the two systems.
In particular, there is a natural correspondence
between the terms used to instantiate existentials in
LL-proofs and the "answers" for the witness variables
provided by the associated LLH-proof.
Notice that it would also be possible to define a variant
of LLH, say LLH', as follows. Rather than requiring partial
answers provided by a candidate proof-tree to be compatible,
one may ask a stronger condition:
for any witness variable Wi, they must all assigne the
SAME value to it.
Then one needs to ``relaxe" the condition on the set of
equations which is premise of an identity rule :
rather then requiring it to represent the MOST GENERAL unifier
of A and A', one just asks it to be AN unifier.
The advange of LLH' over LLH is that it looks more like
a ``standard" proof-system. Its disadvantage is that it does not
really reflect the real process of computation of substitutions.
LLH' does not say HOW to select the correct term ti to be
associated to each occurrence of Wi in the proof, while
systematic calculus of most general unifiers -as done in LLH-
gives an answer to this question.