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