MELD features - Revision history

DavidWhitten at 18:20, 30 September 2019

2019-09-30T18:20:53Z

DavidWhitten: /* Appendix B: Remarks about MELD Implementations */

2019-09-30T17:19:39Z

‎Appendix B: Remarks about MELD Implementations

DavidWhitten at 17:14, 30 September 2019

2019-09-30T17:14:10Z

Show changes

DavidWhitten at 17:11, 30 September 2019

2019-09-30T17:11:38Z

Show changes

DavidWhitten: /* #$BinaryPredicate */

2017-06-09T13:16:08Z

‎#$BinaryPredicate

DavidWhitten: /* ;;; #$BinaryPredicate */

2017-06-09T13:14:44Z

‎;;; #$BinaryPredicate

DavidWhitten: /* ;;; #$AntiSymmetricBinaryPredicate */

2017-06-09T13:13:56Z

‎;;; #$AntiSymmetricBinaryPredicate

DavidWhitten: /* Reifiable vs. Non-Reifiable Functions */

2016-10-16T02:58:18Z

‎Reifiable vs. Non-Reifiable Functions

DavidWhitten: /* Skolemization */

2016-10-16T02:52:31Z

‎Skolemization

DavidWhitten: /* Conventions for permitting/repairing unbound variables in formulas */

2016-10-16T02:45:58Z

‎Conventions for permitting/repairing unbound variables in formulas

@@ Line 7: / Line 7: @@
 Cyc® is a Registered Trademark of Cycorp, Inc.
-This document describes some of the more important features of the [[Moderately Expressive Logical Description]] ([[MELD]]). A formal [[BNF]] will be found in Appendix C, below, but we believe that most prospective users of this language -- for now, that means [[HPKB]] participants and [[Cycorp]] customers -- will find a tutorial document such as this one of more use than that appendix.
+This document describes some of the more important features of the [[Moderately Expressive Logical Description]] ([[MELD]]). A formal [[BNF]] will be found in [[MELD features/Appendix C|Appendix C]], below, but we believe that most prospective users of this language -- for now, that means [[HPKB]] participants and [[Cycorp]] customers -- will find a tutorial document such as this one of more use than that appendix.
 [[MELD]] is a [[formal language]] whose syntax derives from [[first-order predicate calculus]] (the language of [[formal logic]]). In order to express real-world expertise and even just plain old [[common sense knowledge]], however, it goes far beyond [[first order logic]]. The vocabulary of MELD consists of [[terms]]: [[semantic constants]], [[non-atomic terms]] ([[NAT]]s), [[MELD_variables|variables]], numbers, strings, etc. Terms are combined into meaningful [[MELD expressions]], ultimately forming meaningful closed [[MELD sentences]] (with no free variables.) A set of MELD sentences forms a [[knowledge base]]. In this document, for example, we will refer to the [[IKB]], which is the [[DARPA HPKB Integrated Knowledge Base]], and we will refer to the [[Cyc KB]], which is a much larger MELD knowledge base.
-The topmost (most general) content of the [[IKB]] and also of the Cyc KB -- certain abstract terms and the fundamental [[axiom]]s interrelating and using those terms -- forms the kernel of every MELD knowledge base. In fact, the semantics of MELD require and assume the existence of those terms, axioms, etc. (for example, collections such as [[#$Thing]] and [[#$Collection]] and [[#$Predicate]], predicates such as [[#$isa]] and [[#$arg2Isa]], and axioms such as the fact that the [[#$arg2Isa]] of [[#$isa]] is [[#$Collection]].) Those terms (about 160 of them) and assertions (about 650 of them) are part of the definition of MELD, and are listed in this document as Appendix A.
+The topmost (most general) content of the [[IKB]] and also of the Cyc KB -- certain abstract terms and the fundamental [[axiom]]s interrelating and using those terms -- forms the kernel of every MELD knowledge base. In fact, the semantics of MELD require and assume the existence of those terms, axioms, etc. (for example, collections such as [[#$Thing]] and [[#$Collection]] and [[#$Predicate]], predicates such as [[#$isa]] and [[#$arg2Isa]], and axioms such as the fact that the [[#$arg2Isa]] of [[#$isa]] is [[#$Collection]].) Those terms (about 160 of them) and assertions (about 650 of them) are part of the definition of MELD, and are listed in this document as [[MELD features/Appendix A|Appendix A]].
-Every MELD implementation is likely to make some choices, and add some special purpose code, for efficiency's sake. MELD is a purely declarative language, hence those issues are orthogonal (or meta-) to the specification of MELD. However, as a help to real flesh and blood MELD users and implementors, we've collected some of the most important main remarks about this topic as Appendix B.
+Every MELD implementation is likely to make some choices, and add some special purpose code, for efficiency's sake. MELD is a purely declarative language, hence those issues are orthogonal (or meta-) to the specification of MELD. However, as a help to real flesh and blood MELD users and implementors, we've collected some of the most important main remarks about this topic as [[MELD features/Appendix B|Appendix B]].
 = Contents: =
@@ Line 136: / Line 136: @@
 is not [[well-formed]], since the arity of isa is 2, but this formula gives it 3 arguments.
-The arity of a predicate is a semantic constraint imposed by making an assertion to the KB, in MELD, of the form '''(''' [[#$#$arity]] [[#$likesAsFriend]] 2''')''', '''('''[[#$arity]] [[#$between]] 3''')''', etc. The '''('''[[#$#$arity]]  . . . ''')''' assertions for the predicates which are part of the [[MELD KERNEL KB]] are also all a part of that [[KERNEL KB]]; see Appendix B.
+The arity of a predicate is a semantic constraint imposed by making an assertion to the KB, in MELD, of the form '''(''' [[#$#$arity]] [[#$likesAsFriend]] 2''')''', '''('''[[#$arity]] [[#$between]] 3''')''', etc. The '''('''[[#$#$arity]]  . . . ''')''' assertions for the predicates which are part of the [[MELD KERNEL KB]] are also all a part of that [[KERNEL KB]]; see [[MELD features/Appendix B|Appendix B]].
 For example, '''('''[[#$arity]] [[#$isa]] 2''')'''. Since arity is itself one of those predicates, there is an assertion about the arity of arity, namely '''('''[[#$arity]] [[#$arity]] 2''')'''.
@@ Line 327: / Line 327: @@
 Note that this connective takes exactly 2 arguments, and of course their order matters quite a bit. However, one cannot distinguish '''('''[[#$implies]] formula1 formula2''')''' from logically equivalent formulas such as '''('''[[#$implies]] '''('''[[#$not]] formula2''')''' '''('''[[#$not]] formula1''')'''''')'''. Indeed, this connective is defined in terms of earlier ones ([[#$and]]/[[#$or]]/[[#$not]]).
-Assertions involving implies are very common in MELD knowledge bases (including the [[Cyc KB]] and the [[HPKB IKB]] and, as shown in Appendix A below, even in the tiny [[MELD KERNEL KB]]). We also call these sorts of formulas "conditionals" or "rules", and we often refer to the first argument as the "antecedent" or "if-part" and the second argument as the "consequent" or "then-part".
+Assertions involving implies are very common in MELD knowledge bases (including the [[Cyc KB]] and the [[HPKB IKB]] and, as shown in [[MELD features/Appendix A|Appendix A]] below, even in the tiny [[MELD KERNEL KB]]). We also call these sorts of formulas "conditionals" or "rules", and we often refer to the first argument as the "antecedent" or "if-part" and the second argument as the "consequent" or "then-part".
 Note, however, that the particular formulas above are so simple, and involve so few variables, that they are not representative of assertions likely to be found in [[Cyc]] or in the [[IKB]] or in the [[MELD KERNEL KB]]. We will come to some more representative examples in a moment.
@@ Line 459: / Line 459: @@
 This is not a part of the MELD language itself.
-For more information about this, see Conventions for permitting/repairing unbound variables in formulas in Appendix B.
+For more information about this, see Conventions for permitting/repairing unbound variables in formulas in [[MELD features/Appendix B|Appendix B]].
 ===== [[#$thereExists]] =====
@@ Line 735: / Line 735: @@
 * it may do the opposite (allowing new information to override old).
-In either case, a genuine MELD error should be signaled to the user (via the interface) giving notice of the logical contradiction. This digression into implementation and interface concerns is more properly the subject of Appendix B, below, so we will not pursue it further here.
+In either case, a genuine MELD error should be signaled to the user (via the interface) giving notice of the logical contradiction. This digression into implementation and interface concerns is more properly the subject of [[MELD features/Appendix B|Appendix B]], below, so we will not pursue it further here.
 ==== Default True ====
@@ Line 948: / Line 948: @@
 The support predicate is a way to get at the arguments for a formula.
-{{MELD features/Appendix A}}
+{{:MELD features/Appendix A}}
 = Appendix B: Remarks about MELD Implementations =
@@ Line 1,244: / Line 1,244: @@
-{{MELD features/Appendix C}}
+{{:MELD features/Appendix C}}
 Footnotes

← Older revision		Revision as of 17:19, 30 September 2019
Line 950:		Line 950:
	{{MELD features/Appendix A}}		{{MELD features/Appendix A}}

−	== Appendix B: Remarks about MELD Implementations ==	+	= Appendix B: Remarks about MELD Implementations =

@@ Line 1,055: / Line 1,055: @@
   ''')'''
-=== [[#$BinaryPredicate]] ===
+=== ;;; [[#$BinaryPredicate]] ===
+====#$BinaryPredicate====
   <font color=purple>[[MELD KERNEL KB/17|017]]</font>
   '''('''[[#$isa]] [[#$BinaryPredicate]] [[#$Collection]]''')'''

@@ Line 1,055: / Line 1,055: @@
   ''')'''
-=== ;;; [[#$BinaryPredicate]] ===
+=== [[#$BinaryPredicate]] ===
   <font color=purple>[[MELD KERNEL KB/17|017]]</font>

@@ Line 975: / Line 975: @@
-=== ;;; [[#$AntiSymmetricBinaryPredicate]] ===
+=== [[#$AntiSymmetricBinaryPredicate]] ===
   <font color=purple>[[MELD KERNEL KB/1|001]]</font>
@@ Line 990: / Line 990: @@
      '''('''[[#$isa]] ?SLOT [[#$AsymmetricBinaryPredicate]]''')'''
   ''')'''
 === ;;; [[#$Assertion]] ===

@@ Line 3,903: / Line 3,903: @@
 However, we have found it highly cost-effective to have and use a distinction which is akin to "declaring" certain functions as having their NATs treated more like reified (named) constants.
- In Cyc, e.g., many of the functions (that is, instances of the Collection Function) in its ontology are also asserted to be instances of [[#$ReifiableFunction]], a subset of Function. Each time an instance of ReifiableFunction is used with a new set of arguments to build a NAT, that NAT is instantly reified, that is, preserved in the MELD ontology as a constant. Constants which are reified NATs may or may not immediately inform the asserter of what the name is, or accept a name from them; this is up to the particular user interfaces and application interfaces. It should be the case that a natural-sounding name, of the user's choice, should be assertable later on, just as the user should be given the facility for renaming practically any other constant he/she chooses to rename.
+In Cyc, e.g., many of the functions (that is, instances of the Collection Function) in its ontology are also asserted to be instances of [[#$ReifiableFunction]], a subset of Function. Each time an instance of ReifiableFunction is used with a new set of arguments to build a NAT, that NAT is instantly reified, that is, preserved in the MELD ontology as a constant. Constants which are reified NATs may or may not immediately inform the asserter of what the name is, or accept a name from them; this is up to the particular user interfaces and application interfaces. It should be the case that a natural-sounding name, of the user's choice, should be assertable later on, just as the user should be given the facility for renaming practically any other constant he/she chooses to rename.
 In Cyc, when a new reified NAT-constant is first created, the Cyc implementation of MELD automatically sets up the following correspondence
-    '''('''termOfUnit NAT-CONSTANT NAT-EXPRESSION''')'''
+    '''('''[[#termOfUnit]] NAT-CONSTANT NAT-EXPRESSION''')'''
 where NAT-CONSTANT is the automatically-created constant (probably having some awful name, just like those awful Skolem Function names discussed above) and NAT-EXPRESSION is the non-atomic term that can be used to refer to it.
@@ Line 3,918: / Line 3,918: @@
 It looks like the first and second arguments are the same, but that's because, in lieu of a proper constant name for the reified NAT-constant, the system uses the NAT expression as a print name. If you rename that [[NAT]] later, say to CanadianGovt, then the assertion would appear more like you'd expect:
-    '''('''termOfUnit CanadianGovt '''('''GovernmentFn Canada''')'''''')'''
+    '''('''[[#$termOfUnit]]  '''('''[[#$GovernmentFn Canada''')''' ''')'''
   Also, one could adjust the interface tool to make the internal ugly name appear even before that renaming, so one might see
@@ Line 3,927: / Line 3,927: @@
 A reified NAT can be explicitly identified with an already-existing constant by using the predicate termOfUnit:
-    '''('''termOfUnit TheYear1996 '''('''YearFn 1996''')'''''')'''
+    '''('''[[#$termOfUnit]] [[#$TheYear1996]] '''('''[[#$YearFn]] 1996''')''' ''')'''
-    '''('''termOfUnit Apple '''('''FruitFn AppleTree''')'''''')'''
+    '''('''[[#$termOfUnit]] [[#$Apple]] '''('''[[#$FruitFn]] [[#$AppleTree]]''')''' ''')'''
-When a NAT is identified with a constant using termOfUnit, the two are asserted to be de dicto equivalent. Someone may know about apples, and apple trees, and the bearing of fruit by trees, without knowing that apples are the fruit that comes from apple trees. Of course if they know those concepts using those very English words, it's hard to imagine they don't know where apples come from.
+When a NAT is identified with a constant using [[#$termOfUnit]], the two are asserted to be de dicto equivalent. Someone may know about apples, and apple trees, and the bearing of fruit by trees, without knowing that apples are the fruit that comes from apple trees. Of course if they know those concepts using those very English words, it's hard to imagine they don't know where apples come from.
 Skolem functions are reifiable.

@@ Line 3,871: / Line 3,871: @@
     '''('''[[#$implies
        '''('''[[#$isa]] ?A [[#$Animal]]''')'''
-       '''('''thereExists ?M
+       '''('''[[#$thereExists]] ?M
-          '''('''and '''('''[[#$mother]] ?A ?M''')'''
+          '''('''[[#$and]] '''('''[[#$mother]] ?A ?M''')'''
                   '''('''[[#$isa]] ?M [[#$FemaleAnimal]]''')'''''')''' ''')''' ''')'''
 is canonicalized into four separate, smaller assertions, plus the definition of brand new MELD function called SKF. . ., as follows:
-   '''('''[[#$isa]] [[#$SKF-8675309]] [[#SkolemFunction]] ''')'''
+ '''('''[[#$isa]] [[#$SKF-8675309]] [[#SkolemFunction]] ''')'''
-   '''('''[[#arity]] [[#SKF-8675309]] 1''')'''
+ '''('''[[#arity]] [[#SKF-8675309]] 1''')'''
-   '''('''[[#$implies]]
+ ''('''[[#$implies]]
-     '''('''[[#$isa]] ?A [[$#Animal]] ''')'''
+    '''('''[[#$isa]] ?A [[$#Animal]] ''')'''
-     '''('''mother ?A '''('''[[#$SKF-8675309]] ?A ''')''' ''')''' ''')'''
+    '''('''mother ?A '''('''[[#$SKF-8675309]] ?A ''')''' ''')'''
     '''('''[[#$implies]]
-     '''('''[[#$isa]] ?A [[#$Animal]] ''')'''
+      '''('''[[#$isa]] ?A [[#$Animal]] ''')'''
-     '''('''[[#$isa]] '''('''[[#$SKF-8675309]] ?A ''')''' [[#$FemaleAnimal]] ''')''' ''')'''
+      '''('''[[#$isa]]
 Intuitively, you can think of that new MELD function SKF-8675309 as calculating the mother of its argument. These new functions start out named SKF-. . . because they are Skolem functions. To reiterate: your implementation of MELD may or may not create these functions.

@@ Line 3,761: / Line 3,761: @@
       '''('''[[#$implies]]
           '''('''[[#$isa]] ?W [[#$FemalePerson]]''')'''
-          '''('''loves ?W [[#$Doug]]''')'''
+          '''('''[[#$loves]] ?W [[#$Doug]]''')'''
       ''')'''
   ''')'''