Examples- Higher-Order KIF and Conceptual graphs

fritz@rodin.wustl.edu (Fritz Lehmann)
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

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

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

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

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

[49]. [MARK GRAVES' EXAMPLE] Inter-relation relations in genome

	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,