[Prev][Next][Index][Thread]
Additional reference
Date: Wed, 29 Jul 92 12:25:36 -0400
I just came accross the following interesting book which is extremely
relevant to my recent paper
Constructive Logics. Part I: A Tutorial
on Proof Systems and Typed $\lambda$-Calculi.
This compelled me to update the reference list in my paper by adding:
Normalization, cut-elimination and the theory of proofs, by A. M. Ungar,
CSLI Lecture Notes No. 28 (1992).
The ftp file conslog1.dvi.Z has been updated.
-- Jean
--------------------
The following papers are also available by anonymous ftp:
Unification procedures in automated deduction methods
based on matings: a survey
Jean Gallier
Abstract. Unification procedures arising in methods for
automated theorem proving based on matings are surveyed.
We begin by reviewing some fundamentals
of automated deduction, including the Skolem form and the
Skolem-Herbrand-G\"odel theorem.
Next, the method of matings for first-order
languages without equality due to Andrews and Bibel is presented.
Standard unification is described in terms of transformations on
systems (following the approach of Martelli and Montanari, anticipated
by Herbrand).
Some fast unification algorithms are also
sketched, in particular, a unification closure algorithm inspired
by Paterson and Wegman's method.
The method of matings is then extended to languages with equality.
This extention leads naturally to a generalization of standard
unification called rigid $E$-unification
(due to Gallier, Narendran, Plaisted, and Snyder).
The main properties of
rigid $E$-unification, decidability, NP-completeness, and
finiteness of complete sets, are discussed.
ftp file: gallier/surprov.dvi.Z
-------------------------
Higher-order unification revisited: complete sets
of transformations
Jean Gallier and Wayne Snyder
Abstract. In this paper, we reexamine the problem of
general higher-order unification
and develop an approach based on the method of
transformations on systems of terms which has its roots in Herbrand's
thesis, and which was developed by Martelli and Montanari
in the context of first-order unification.
This method provides an abstract and mathematically elegant means of
analyzing the invariant properties of unification in
various settings by providing a clean separation of the logical issues
>from the specification of procedural information.
Our major contribution is three-fold. First, we have extended
the Herbrand-Martelli-Montanari method of transformations on systems
to higher-order unification and pre-unification; second,
we have used this formalism to provide a more direct
proof of the completeness of a method for higher-order unification
than has previously been available; and, finally, we have shown
the completeness of the strategy of eager variable elimination.
In addition, this analysis provides another justification of the
design of Huet's procedure, and shows how its basic principles
work in a more general setting.
Finally, it is hoped that this presentation might form a good
introduction to higher-order unification for those readers
unfamiliar with the field.
ftp file: gallier/hounif.dvi.Z
-------------------------
Designing Unification Procedures Using Transformations:
A Survey
Jean Gallier and Wayne Snyder
ftp file: gallier/survey.dvi.Z
-------------------------
@article(gallsny89,
author = "Gallier, J. and Snyder, W.",
title ="Higher-order unification revisited: complete sets
of transformations",
journal = "J. Symbolic Computation"
year = "1989",
volume="8",
pages="101--140")
@INCOLLECTION{GallSny91
, AUTHOR = {Gallier, J. and Snyder, W.}
, TITLE = {Designing Unification Procedures Using Transformations:
A Survey}
, BOOKTITLE = {Logic From Computer Science}
, PUBLISHER = {Springer Verlag}
, YEAR = {1991}
, EDITOR = {Y. Moschovakis}
, PAGES = {153-215}
, ADDRESS = {New York}
}
@techreport(gallier91tr,
Author="Gallier, J.",
Title="Unification procedures in automated deduction methods
based on matings: a survey",
Year=1991,
Institution="Computer Science Department, University of
Pennsylvania",
number="?",
Note="To appear in a book edited by M. Nivat and A. Podelski, 1993")
-------------------------
The above paper(s) can be retrieved by anonymous ftp using the
instructions below.
% ftp ftp.cis.upenn.edu
Name: anonymous
Password: <<your e-mail address>>
ftp> cd pub/papers/gallier
ftp> binary
ftp> get filename.dvi.Z
ftp> quit
Then, use the unix "uncompress" command on this file to
get the dvi file(s).
-- Jean