[Prev][Next][Index][Thread]
Herbrand methods in Linear Logic (revised)
Date: Thu, 06 Feb 92 11:07:17 -0800
This revises a posting to linear@cs.stanford.edu. The correct
ftp site is ftp.csl.sri.com.
__________________________________________________________________
Cerrito's message has prompted me to advertise a paper of mine on proof
search in the intuitionistic sequent calculus to be presented at CADE-11
in June. (The work was actually done in 1987/88 and was also
implemented in Scheme.)
My impression is that it is a very traditional idea to use Herbrand
variables to replace (essentially) existential quantifiers, Herbrand
functions to replace (essentially) universal quantifiers, and
unification (with occurs-check to enforce the eigenvariable condition),
for cut-free proof search in arbitrary sequent calculi. What I present
is a systematic way of optimizing the use of Herbrand functions so that
they do not depend on ALL the Herbrand variables but only some essential
subset, namely those that are required in order to record certain
impermutable inference steps. This leads to a dramatic reduction in the
amount of backtracking in naive proof search while retaining all the
other nice properties of proof search. While I only treat
intuitionistic sequent calculus, I believe that the technique is easily
adapted for other cut-free sequent calculi that have conventional
quantifier rules by identifying the impermutable pairs of inference
rules. (Pat Lincoln posted the table corresponding to linear logic to
this list, and I think Bellin has also identified these
impermutabilities.) The fact that all the propositional inferences in
classical logic are permutable is the key to the Herbrand theorem there.
The work of Wallen (Automated deduction in nonclassical logics, MIT
Press, 1989), and Pym and Wallen (CADE10) is closely related, but
neither of these use the Herbrand terms to encode the impermutabilities.
I'd like to be informed of any other related work.
__________________________________________________________________
The paper can be obtained via anonymous ftp from ftp.csl.sri.com
(with type binary) as the file /pub/shankar-cade92.dvi.
__________________________________________________________________
Title: Proof Search in the Intuitionistic Sequent Calculus
Author: Natarajan Shankar, SRI Computer Science Laboratory,
Menlo Park CA94025 USA
Abstract:
The use of Herbrand functions (more popularly known as {\it
Skolemization\/}) plays an important role in classical theorem proving
and logic programming. We define a notion of Herbrand functions for the
full intuitionistic predicate calculus. The definition is based on the
view that the proof-theoretic role of Herbrand functions (to replace
universal quantifiers), and of unification (to find instances
corresponding to existential quantifiers), is to ensure that the
eigenvariable conditions on a sequent proof are respected. The
propositional impermutabilities that arise in the intuitionistic but not
the classical sequent calculus motivate a generalization of the
classical notion of Herbrand functions. Proof search using generalized
Herbrand functions also provides a framework for generalizing logic
programming to subsets of intuitionistic logic that are larger than Horn
clauses. The search procedure described here has been implemented and
observed to work effectively in practice. The generalization of
Herbrand functions can also be applied to sequent calculi formalizations
of logics other than intuitionistic predicate calculus.