Logic with partial functions?

Steffo Weber

unread,

Mar 1, 1995, 7:11:00 AM3/1/95

to

|> Can anybody point me to references on first-order
|> logic with partial functions? It's much appreciated.

Take a look at Kleene's (strong) 3-valued logic in
"Introduction to metamathematics"

--steffo!

H. Enderton

unread,

Mar 1, 1995, 6:12:09 PM3/1/95

to

hx...@saul.cis.upenn.edu (Hong-liang Xie) writes:
>Can anybody point me to references on first-order
>logic with partial functions? It's much appreciated.

If you mean logic where terms don't need to denote anything,
that's usually called "free logic." Searching for that
phrase will probably turn up specific references. (Free
logic also does not require the domain of discourse to be
nonempty.)

--Herb Enderton (h...@math.ucla.edu)

Middelburg C.A.

unread,

Mar 2, 1995, 2:38:12 AM3/2/95

to

In article <3j0i8g$r...@netnews.upenn.edu>,

hx...@saul.cis.upenn.edu (Hong-liang Xie) writes:
|> Can anybody point me to references on first-order
|> logic with partial functions? It's much appreciated.
|>

Below you find some references in BiBTeX format.

A range of approaches to deal with partial functions are
reviewed in [CJ91] and [MR91]. A recent and comprehensive
description of LPF (Logic of Partial Functions) is given
in [JM94]. The oldest reference is probably [Kle52].

Best regards,

Kees Middelburg

P.S. [MR91] and [JM94] are available in PostScript format
by FTP: ftp://ftp.phil.ruu.nl/pub/logic/keesm/
by WWW: http://www.phil.ruu.nl/home/keesm/

@article{Avr91,
author = "A. Avron",
title = "Natural 3-valued Logics {--} Characterization and Proof Theory",
journal = "Journal of Symbolic Logic",
volume = 56, year = 1991, pages = "276--294"}

@article{BCJ84,
author = "H. Barringer and J.H. Cheng and C.B. Jones",
title = "A Logic Covering Undefinedness in Program Proofs",
journal = "Acta Informatica",
volume = 21, year = 1984, pages = "251--269"}

@book{Bee85,
author = "M.J. Beeson",
title = "Foundations of Constructive Mathematics",
publisher = "Springer Verlag",
year = 1985}

@article{Bee88,
author = "M.J. Beeson",
title = "Towards a Computation System Based on Set Theory",
journal = "Theoretical Computer Science",
volume = 60, year = 1988, pages = "297--340"}

@incollection{Bla86,
author = "S. Blamey",
title = "Partial Logic",
booktitle = "Handbook of Philosophical Logic, Volume~III",
editor = "D. Gabbay and F. Guenther",
publisher = "D. Reidel Publishing Company",
year = 1986, chapter = "III.1"}

@phdthesis{Che86,
author = "J.H. Cheng",
title = "A Logic for Partial Functions",
school = "University of Manchester, Department of Computer Science",
note = "Technical Report UMCS-86-7-1",
year = 1986}

@inproceedings{CJ91,
author = "J.H. Cheng and C.B. Jones",
title = "On the Usability of Logics which handle Partial Functions",
booktitle = "3rd Refinement Workshop",
editor = "C. Morgan and J.C.P. Woodcock",
publisher = "Springer Verlag, Workshops in Computing Series",
year = 1991, pages = "51--69"}

@article{GL90,
author = "A. {Gavilanes-Franco} and F. {Lucio-Carrasco}",
title = "A First Order Logic for Partial Functions",
journal = "Theoretical Computer Science",
volume = 74, year = 1990, pages = "37--69"}

@book{GMW79,
author = "M.J.C. Gordon and R. Milner and C. Wadsworth",
title = "Edinburgh LCF",
publisher = "Springer Verlag, LNCS~78",
year = 1979}

@article{Hol91,
author = "M. Holden",
title = "Weak Logic Theory",
journal = "Theoretical Computer Science",
volume = 79, year = 1991, pages = "295--321"}

@article{Hoo87,
author = "A. Hoogewijs",
title = "Partial-Predicate Logic in Computer Science",
journal = "Acta Informatica",
volume = 24, year = 1987, pages = "381--393"}

@article{JM94,
author = "C.B. Jones and C.A. Middelburg",
title = "A Typed Logic of Partial Functions Reconstructed Classically",
journal = "Acta Informatica",
volume = 31, year = 1994, pages = "399--430"}

@book{Kle52,
author = "S.C. Kleene",
title = "Introduction to Metamathematics",
publisher = "North-Holland",
year = 1952}

@inproceedings{KTB88,
author = "B. Konikowska and A. Tarlecki and A. Blikle",
title = "A Three-valued Logic for Software Specification and Validation",
booktitle = "VDM~'88",
editor = "R. Bloomfield and L. Marshall and R. Jones",
publisher = "Springer Verlag, LNCS~328",
year = 1988, pages = "218--242"}

@inproceedings{KR89,
author = "C.P.J. Koymans and {Renardel de Lavalette}, G.R.",
title = "The Logic {$\mbox{MPL}\sb\omega$}",
booktitle = "Algebraic Methods: Theory, Tools and Applications",
editor = "M. Wirsing and J.A. Bergstra",
publisher = "Springer Verlag, LNCS~394",
year = 1989, pages = "247--282"}

@incollection{Luk67,
author = "J. {\L}ukasiewicz",
title = "On Three-valued Logic",
booktitle = "Polish Logic 1920--1939",
editor = "S. McCall",
publisher = "Oxford University Press",
year = 1967}

@incollection{McC67,
author = "J. McCarthy",
title = "A Basis for a Mathematical Theory of Computation",
booktitle = "Computer Programming and Formal Systems",
editor = "P. Braffort and D. Hirschberg",
publisher = "North-Holland Publishing Company",
year = 1967, pages = "33--70"}

@inproceedings{MR91,
author = "C.A. Middelburg and {Renardel de Lavalette}, G.R.",
title = "{LPF} and {$\mbox{MPL}\sb\omega$} {--}
A Logical Comparison of {VDM SL} and {COLD-K}",
booktitle = "VDM~'91, Volume~1",
editor = "S. Prehn and W.J. Toetenel",
publisher = "Springer Verlag, LNCS~551",
year = 1991, pages = "279--308"}

@book{Pau87,
author = "L.C. Paulson",
title = "Logic and Computation",
publisher = "Cambridge University Press,
Cambridge Tracts in Theoretical Computer Science 2",
year = 1987}

@unpublished{Plo85,
author = "G.D. Plotkin",
title = "Partial Function Logic",
note = "Lectures at Edinburgh University",
year = 1985}

@article{Ren84,
author = "{Renardel de Lavalette}, G.R.",
title = "Descriptions in Mathematical Logic",
journal = "Studia Logica",
volume = 43, year = 1984, pages = "281--294"}

@inproceedings{Sco67,
author = "D.S. Scott",
title = "Existence and Description in Formal Logic",
booktitle = "Bertrand Russell, Philosopher of the Century",
editor = "R. Schoenman",
publisher = "Allen {\&} Unwin",
year = 1967, pages = "181--200"}

@inproceedings{Sco79,
author = "D.S. Scott",
title = "Identity and Existence in Intuitionistic Logic",
booktitle = "Applications of Sheaves",
editor = "M.P. Fourman and C.J. Mulvey and D.S. Scott",
publisher = "Springer Verlag, Lecture Notes in Mathematics~753",
year = 1979, pages = "660--696"}

--
----- Dept NSC, KPN Research, P.O. Box 421, 2260 AK Leidschendam, NL. -----
Dept of Philosophy, Utrecht University, P.O.Box 80126, 3508 TC Utrecht, NL.
--------------- FTP: ftp://ftp.phil.ruu.nl/pub/logic/keesm/ ---------------
----------------- WWW: http://www.phil.ruu.nl/home/keesm/ -----------------

Claus Hintermeier

unread,

Mar 2, 1995, 5:40:31 AM3/2/95

to

Try this one for an intuitionistic version:

@InProceedings{Scott77,
author = "Scott, D. S.",

title = "Identity and Existence in Intuitionistic Logic",
booktitle = "Applications of Sheaves",

publisher = "Springer-Verlag",
year = "1977",
series = "Lecture Notes in Mathematics",
volume = 753,
editor = "M. P. Fourman and C. J. Mulvey ",
pages = "660--696",
}

`Hope this helps,

Claus.
--
*******************************************************************************
* *
* Claus Hintermeier email: hint...@loria.fr *
* CRIN/INRIA Lorraine tel. : (+33) 83.59.20.22 *
* BP 239 fax : (+33) 83.27.83.19 *
* F-54506 Vandoeuvre-les-Nancy CEDEX *
* France *
* *
*******************************************************************************

Hong-liang Xie

unread,

Feb 28, 1995, 8:22:24 PM2/28/95

to

Can anybody point me to references on first-order
logic with partial functions? It's much appreciated.

Thanks,

Hong

Stephen J. Garland

unread,

Mar 3, 1995, 10:51:41 AM3/3/95

to

A fully worked-out approach to logic with partial functions can be found in the work
being done on IMPS at Mitre. Information about IMPS is available on the Web at
file://math.harvard.edu/imps/imps_html/imps.html
and in the following articles:

@Article{Farmer90,
author = "W. M. Farmer",
title = "A Partial Functions Version of {Church's} Simple
Theory of Types",

journal = "Journal of Symbolic Logic",

year = "1990",
volume = "55",
Optnumber = "3",
pages = "1269-91",
OPTmonth = "",
OPTnote = "Also {\sc mitre} Corporation technical report M88-52,
1988; revised 1990."
}
@Article{Farmer93b,
author = "W. M. Farmer",
title = "A Simple Type Theory with Partial Functions and Subtypes",
journal = "Annals of Pure and Applied Logic",
year = "1993",
volume = "64",
OPTnumber = "3",
pages = "211--240",
OPTmonth = "",
OPTnote = ""
}
@InProceedings{FarmerEtAl92a,
author = "W. M. Farmer and J. D. Guttman and F. J. Thayer",
title = "{\sc imps}: System Description",
booktitle = "Automated Deduction---CADE-11",
year = "1992",
series = "Lecture Notes in Computer Science",
volume = "607",
editor = "D. Kapur",
pages = "701--705",
OPTorganization = "",
publisher = "Springer-Verlag",
OPTaddress = "",
OPTmonth = "",
OPTnote = ""
}
@Article{FarmerEtAl93,
author = "W. M. Farmer and J. D. Guttman and F. J. Thayer",
title = "{\sc imps}: an {I}nteractive {M}athematical {P}roof {S}ystem",
journal = "Journal of Automated Reasoning",
year = "1993",
volume = "11",
OPTnumber = "2",
pages = "213--248",
OPTmonth = "October"
}

Manfred Kerber

unread,

Mar 6, 1995, 4:05:12 AM3/6/95

to

We have elaborated a mechanization of a three-valued approach based on
strong Kleene logic.

@INPROCEEDINGS{KeKo94-CADE,
AUTHOR = {Manfred Kerber and Michael Kohlhase},
TITLE = {A Mechanization of Strong {K}leene Logic for Partial Functions},
BOOKTITLE = {Proceedings of the 12th CADE},
YEAR = {1994},

EDITOR = {Alan Bundy},
PAGES = {S.~371--385},
ORGANIZATION = {},
PUBLISHER = {Springer Verlag, Berlin, Germany},
ADDRESS = {Nancy, France},
MONTH = {},
NOTE = {LNAI 814},
STATUS = {}}

You can find the paper also in the World Wide Web under
http://js-sfbsun.cs.uni-sb.de/pub/papers/abstracts.html#KeKo94-CADE.bib

Manfred

Cliff B Jones

unread,

Mar 15, 1995, 3:21:32 AM3/15/95

to

|> hx...@saul.cis.upenn.edu (Hong-liang Xie) writes:
|> >Can anybody point me to references on first-order
|> >logic with partial functions? It's much appreciated.

I don't keep up with this group so it is possible these references have already
been posted

A useful survey:

@inproceedings{ChengJones91,
author = "J. H. Cheng and C. B. Jones",
title = "On the usability of logics which handle
partial functions",

booktitle = "3rd Refinement Workshop",
editor = "C. Morgan and J. C. P. Woodcock",

pages = "51--69",
publisher = "Springer-Verlag",
year = "1991"
}

A recent paper on the foundations of LPF:
@article{JonesMiddelburg94,

author = "C.B. Jones and C.A. Middelburg",
title = "A Typed Logic of Partial Functions Reconstructed
Classically",
journal = "Acta Informatica",
volume = 31,

number = 5,
pages = "399--430",
year = 1994
}

The first of our papers on LPF:
@article{BCJ84,
author = "H. Barringer and J.H. Cheng and C. B. Jones",

title = "A Logic Covering Undefinedness in Program Proofs",

journal = acta,
volume = "21",
pages = "251--269",
year = "1984"
}

Jen Cheng's thesis:
@phdthesis{Cheng86,
title = "A Logic for Partial Functions",

author = "J.H. Cheng",

school = "University of Manchester",
year = "1986"
}