**Mail folder:**Interlingua Mail**Next message:**phayes@cs.uiuc.edu: "Re: A proposal of "sorts""**Previous message:**Tony Sarris: "Correction w.r.t 'otology'"**Reply:**phayes@cs.uiuc.edu: "Re: A proposal of "sorts""**Reply:**phayes@cs.uiuc.edu: "Re: A proposal of "sorts""**Reply:**phayes@cs.uiuc.edu: "Re: A proposal of "sorts""

Date: Fri, 3 Dec 93 21:16:47 -0800 From: Tomas Uribe <uribe@CS.Stanford.EDU> Message-id: <9312040516.AA27752@Xenon.Stanford.EDU> To: Interlingua-working-group@ISI.EDU Subject: A proposal of "sorts" Cc: uribe@cs.stanford.edu

To the Interlingua Working Group: this is a draft proposal concerning the issue of sorts and types in KIF. Please send me any comments that you may have. Once all objections are sorted out (pun intended) we can send this out to the Interlingua list. Thanks, - Tomas E. Uribe uribe@CS.Stanford.EDU ========================================================================== While the discussion on first vs. higher-order logic simmers on the Interlingua list, I would like to go back to an earlier (and simpler!) issue: whether typed variables should be included in KIF. As far as KIF is concerned, the question is whether types should be part of the syntax or viewed as unary predicates. I propose the latter alternative as being the simplest and more flexible one. It is true, as Fritz Lehmann has pointed out, that sorts can be very useful in speeding up automated deduction; they can also help make axiomatizations more readable, compact and natural. However, all of these advantages can be retained even if sorts are seen as "only" syntactic sugar for unary predicates. The only obstacle, perhaps, is that sorts may have to be extracted automatically from axiomatizations---but this can be done without much trouble (this was done in, for instance, the Markgraf Karl theorem prover [3],[4].) Building sorts into the syntax has the main disadvantage that either (a) the set of sorts has to be fixed beforehand with no possibility of extension, or (b) a standard language for defining sorts has to be decided on. (a) is clearly too limiting; but (b) is too: Many systems use sorts, but different systems handle different kinds! Some choose less expressive ones at the advantage of speedier sort inference; others allow for more expressive sorts that require more complex and specialized inference mechanisms. What kind of sorts would we want to allow? Will the sorted logic be many-sorted, order-sorted, monomorphic, polymorphic, static, dynamic? What kind of declarations would be used? We can simply allow for the most general mechanism commonly used for defining sorts, namely, the axiomatization of unary predicates in first-order logic (see e.g. [1], [2]). Note that even when sorts are built into the syntax, the equivalent effect is obtained through a "relativization" theorem (e.g. [5]). Systems can be free to translate some or all of these unary predicates into whatever sort structures they can handle; and systems that make no provision for sorts will be happy too. ============================================================================ The proposal is then to use restricted quantifiers as follows: Add, as syntactic sugar to quantifiers, the constructions (exists ((?x P)) <Sentence>) and (forall ((?x P)) <Sentence>) as abbreviations for (exists (?x) (=> P(?x) <Sentence>)) and (forall (?x) (=> P(?x) <Sentence>)). In general, (<quantifier> ((?x1 P1) .. (?xN PN)) <Sentence>) abbreviates (quantifier (?x1 ...?xn) (=> (and P1(?x1) ... PN(?xN)) <Sentence>)) A warning: there is the well-known "empty sort problem:" Just writing [1] (exists ((?x P)) <Sentence>(?x)) does not ensure that [2] (exists (?x) <Sentence>(?x)) is true, since [3] (exists (?x) P(?x)) may be false, so that [1] is trivially true. That a "sort" is non-empty can be ensured simply by asserting [3] for every appropriate predicate P. (In any case, it sometimes may be desirable to allow for empty sorts---see [1].) ========================================================================== References: [1] A. G. Cohn, "A Many-Sorted Logic with Possibly Empty Sorts", in CADE-11, pp. 633-647, volume 607 of Lecture Notes in AI, Springer-Verlag, 1992. [2] Alan M. Frisch, "The Substitutional Framework for Sorted Deduction: Fundamental Results on Hybrid Reasoning", Artificial Intelligence 49:161--198, 1991. [3] Hans-Jurgen Ohlbach and Jorg Siekmann, "The Markgraph Karl Refutation Procedure", in Computational Logic: Essays in honor of Alan Robinson (Lassez and Plotkin, eds.), pp. 41-112, 1991. [4] Manfred Schmidt-Shauss, "Mechanical Generation of Sorts in Clause Sets", SEKI report 85-VI-KL, Fachbereich Informatik, Universitat Kaiserslautern, Germany, 1985. [5] Manfred Schmidt-Shauss, "Computational Aspects of an Order-Sorted Logic with Term Declarations", volume 395 of Lecture Notes in AI, Springer-Verlag, 1989. ========================================================================== - Tomas E. Uribe uribe@CS.Stanford.EDU