**Mail folder:**Interlingua Mail**Next message:**phayes@cs.uiuc.edu: "Re: Higher-Order KIF and Conceptual Graphs"**Previous message:**Fritz Lehmann: "Higher-Order KIF and Conceptual Graphs"**Reply:**Dan Schwartz: "Examples- Higher-Order KIF and Conceptual graphs"**Reply:**Tom Gruber: "high order relations in first order KIF"

Reply-To: cg@cs.umn.edu Date: Thu, 11 Nov 93 08:25:31 CST From: fritz@rodin.wustl.edu (Fritz Lehmann) Message-id: <9311111425.AA10829@rodin.wustl.edu> To: boley@dfki.uni-kl.de, cg@cs.umn.edu, interlingua@isi.edu Subject: Examples- Higher-Order KIF and Conceptual graphs

I've been asked by a few people to re-list my "about five or six" earlier email examples which might call for higher- order treatment. Actually it's closer to 50 examples by now, though not all are good test cases. Since I started this thread in September, I've mentioned the following examples as being at least potentially higher-order. Not all of these require strongly higher-order formal semantics. Some do. The rest can be handled with (varying degrees of) "syntactic sugar". When this is possible can be a subtle question. 1. "Aristotle has all the virtues of a philosopher." 2. Patrick Winston's relation-between-relations semantic net link [between the "left-of" and "right-of" relational links]. 3. The IS-A link in inheritance and subsumption hierarchies. [as a relation or link, not a set of FO axioms] 4. The relational IS-A/subsumption link in relational hierarchies. [some arguments may be permuted] 5. The formal definition of individual identity or equality. [As in "x = y =def= Ax,y AP (P(x) iff P(y)).] 6. The assertion that, for a particular individual, all of a certain kind of functions on that individual take a certain kind of value. [including recursively defined functions] 7. The ability to refer to and predicate the relations which exist between a given relation and its own arguments. For R(a,b), this yields R'(a,R); R''(b,R,R'); and infinitely more. 8. Semantic "case relation" taxonomy links. 10. The inclusion ordering in cylindric algebras. 11. The type lattice on Conceptual Graphs relations [circles]. 12. Closure of the universe under classes and disjoint unions of direct products. 13. Harold Boley's Directed Recursive Labelnode Hypergraphs [under closure]. 14. The meanings of, and explicit relations among, the "columns" of a [relational] database. 15. Relations in hierarchies of Rudolf Wille's Concept Lattices. 16. In Euclidean Between(a,b,c), the qualities of a's relation to the betweenness lacked by b's and c's [relations to the betweenness]. 17. The semantics of the named [perhaps semantically indexed, and predicable] "argument positions" of any relation in Jim Fulton's Semantic Unification Meta-Model (SUMM). 18. (In Conceptual Graphs) For Sowa's individual x, some reified [PREDICATE: p] or [TYPE: p], and assertion P(x), --- the formal model-theoretic semantics that would let us know that p=P. 19. In Tom Gruber's Ontolingua, the formal semantics of second- order relations. The formal semantic difference, if any, between (type Tx) and (chair Tx). 20. Peirce's "hypostatic abstraction" or reifying relations into individuals, but retaining their essential relational character. 21. "North is the opposite of South" [the point here being the "opposite", not some converseness axioms about directions] 22. "The thief is to robbery what the beloved is to love." [i.e. each individual stands in the same kind of relation to the respective (different) relations.] 23. "Bart has all the virtues of a philosopher." [Similar in form, if not truth value, to example no. 1] [24]. [PAT HAYES' EXAMPLE] Beta-reduction of lambda sentences, the form being "(lambda x.PHI[x]) (t) IFF PHI(t) for any WFF PHI and term t". 25. Peirce's (or Leibniz's) sentence "Given any two things, there is some character which one posseses and the other does not." [Needed to distinguish among differing "individual distinctness" criteria of different knowledge bases. Distinctness of individuals not to be assumed already (in the formal interpretation of this sentence).] [26]. [PAT HAYES' EXAMPLE?] Real number line without non- standard models. [FO can't specify this.] 27. Being able to mention 100 senators without having to list 4,950 explicit inequalities between pairs of senators, as in FOL. [If 'sugared', the sugar has to be pretty strong.] 28. Defining equality formally by schema of FOL sentences on finite vocabulary of Relations X No. of Argument-places, when some relations have no fixed arities. [My answer to Hayes' answer to no. 5.] 29. The [ever-present] relation in Category Theory between a natural transformation and the relation between an affected morphism and one of its participating objects. 30. Ontek Inc.'s 3rd and 4th order predicates. 31. "All monotonic functions of 42 have positive values." [Seems mundane, but don't neglect the recursive weirdos.] 32. Relations defined on connectives, as in work of Zellweger, Menger or Stern. [Not sure logic-order is the issue here.] [33]. [DAN SCHWARTZ'S EXAMPLE] Combination of classical outer logic with fuzzy inner logic. [This initially strikes me as a meta-level issue rather than a logic-order issue.] [34]. [DAN SCHWARTZ'S EXAMPLE] Combination of quantification, likelihood, and usuality. [Same comment.] 35. Formalizing distinction among First-Order/set-based, higher-order/approximative/intesional, and inchoative systems. [See example 25 above.] 36. Formalizing higher-order factorizations of large-scale structure of concept hierarchy. 37. Formal semantic definition of the predicate "infinite". 38. Formal semantic definition of "countable sets". 39. Formal semantic definition of "well-orderings". 40. Formal semantic definition of "natural numbers". 41. Formal semantic definition of "real numbers". 42. Formal semantic definition of the classifying properties of ordered Abelian groups. 43. Formal semantic definition of the classifying properties of various kinds of automata. [incl. Buchi.] 44. Formal semantic definition of the classifying properties of classes of [potentially infinite] trees. 45. Formal semantic definition of topological, compact and Hausdorff spaces. 46. Formal semantic definition of the classifying properties of complete partial and linear orders, lattices, and Boolean algebras. 47. Formal semantic definition of the classifying properties of Scott-type domains. [incl. in 46] 48. Formal semantic definition of the classifying properties of various kinds of probabilistic systems. [incl. probabilistic quantifiers]. [49]. [MARK GRAVES' EXAMPLE] Inter-relation relations in genome mapping. This list could be shortened considerably by removing some examples which are essentially duplicates and those which can simply be handled correctly in First-Order logic. One could add candidate examples too, (like complex algebras, Chris Brink's Power Structures, and the refinement order on partitions ?) Since September, of these, Sowa has addressed in Conceptual Graphs one (no. 25), the KIF authors, none.