Papers on alternative type theory logics for NL semantics

[Shalom Lappin]

Hi Glyn,
     You may be interested in a series of three papers which Chris Fox,
Carl, and I presented at the Natural Language Understanding and Logic
Programming Workshop in Copenhagen in June and at LoLa7 in Pecs in
August.  In Fox, Lappin, and Pollard (2002a)  ("First-Order Curry-Typed
Logic for Natural Language Semantics" in S. Wintner (ed.), Proceedings
of the Seventh Workshop on Natural Language Understanding and Logic
Programming, Copenhagen,  pp. 175-192) and  Fox, Lappin, and Pollard
(2002b) ( “Intensional First-Order Logic with Types” in G. Alberti, K.
Balough, and P. Dekker (eds.),   Proceedings of the Seventh Symposium
for Logic and Language, Pecs, Hungary, pp. 47-56) we present an extended
first-order Property Theory with flexible Curry typing to allow for
subtypes, dependent types, and polymorphism. We have specified both
natural deduction rules and a tableaux proof procedure for this sytem,
and we have worked out the initial outline of a model theory. The sketch
of the model theory does not appear in the papers, but it is availabe in
slides for an upcoming talk. In Fox, Lappin, and Pollard (2002c) ( “A
Higher-Order Fine-Grained Logic for Intensional Semantics” in G.
Alberti, K. Balough, and P. Dekker (eds.), Proceedings of the Seventh
Symposium for Logic and Language, Pecs, Hungary, pp.37-46) we give a
higher-order intensional logic with Church typing, a tableaux proof
theory, and a fully worked out algebraic semantics. Both type logics are
radically intensional and represent intensions independentlly of
possible worlds. They both sustain alpha, beta, and eta reduction while
avoiding the entailment from provable extensional equivalence to
intensional identity.  The papers are available on my web site at
http://www.dcs.kcl.ac.uk/staff/lappin/, and on Chris' web site at
http://cswww.essex.ac.uk/staff/foxcj/. Regards.
                                              Shalom