;; Kownledge base for the amusing friend demo.

;;;;;;;;;;;;;
;; Honesty ;;
;;;;;;;;;;;;;

;; Probability of being honest
(Predicate "is-honest" (stv 0.8 0.9))

;; Probability that two things are honest
;;
;; This should be inferred since we don't have the rules to infer that
;; we put it in the kb for now.
(Lambda (stv 0.64 0.9)
   (VariableList
      (TypedVariable
         (Variable "$X")
         (Type "ConceptNode"))
      (TypedVariable
         (Variable "$Y")
         (Type "ConceptNode")))
   (And
      (Evaluation
         (Predicate "is-honest")
         (Variable "$X"))
      (Evaluation
         (Predicate "is-honest")
         (Variable "$Y"))))

;; Probability of telling the truth to someone. The probability if
;; very low cause the probability of telling something to someone is
;; already very low.
(Predicate "told-the-truth" (stv 0.00001 0.7))

;; We need also the following. It should normally be wrapped in a
;; Lambda, but because instantiation. And ultimately this should be
;; inferred.
(Evaluation (stv 0.00001 0.7)
   (Predicate "told-the-truth-about")
   (List
      (Variable "$X")
      (Variable "$Y")
      (Variable "$Z")))

;; People who told the truth about something are honest
(define people-telling-the-truth-are-honest
(ImplicationScope (stv 0.95 0.9)
   (VariableList
      (TypedVariable
         (Variable "$X")
         (Type "ConceptNode"))
      (TypedVariable
         (Variable "$Y")
         (Type "ConceptNode"))
      (TypedVariable
         (Variable "$Z")
         (Type "ConceptNode")))
   (Evaluation
      (Predicate "told-the-truth-about")
      (List
         (Variable "$X")
         (Variable "$Y")
         (Variable "$Z")))
   (Evaluation
      (Predicate "is-honest")
      (Variable "$X"))))

;;;;;;;;;;;;;;
;; Humanity ;;
;;;;;;;;;;;;;;

;; Probability of two human acquaintances
(Lambda (stv 0.0002 0.9)
   (VariableList
      (TypedVariable
         (Variable "$X")
         (Type "ConceptNode"))
      (TypedVariable
         (Variable "$Y")
         (Type "ConceptNode")))
   (And
      (Inheritance
         (Variable "$X")
         (Concept "human"))
      (Inheritance
         (Variable "$Y")
         (Concept "human"))
      (Evaluation
         (Predicate "acquainted")
         (List
            (Variable "$X")
            (Variable "$Y")))))

;;;;;;;;;
;; Bob ;;
;;;;;;;;;

;; Bob is a human
(Inheritance (stv 1 1)
   (Concept "Bob")
   (Concept "human"))

;;;;;;;;;;
;; Self ;;
;;;;;;;;;;

;; I am a human
(Inheritance (stv 1 1)
   (Concept "Self")
   (Concept "human"))

;; I am honest
(Evaluation (stv 0.9 0.9)
   (Predicate "is-honest")
   (Concept "Self"))

;; I know Bob
(Evaluation (stv 1 1)
   (Predicate "acquainted")
   (List
      (Concept "Self")
      (Concept "Bob")))

;;;;;;;;;;;;;;;;
;; Friendship ;;
;;;;;;;;;;;;;;;;

;; The probability of random things (typically humans) being friends
(Predicate "will-be-friends" (stv 0.0001 0.9))

;; Friendship is symmetric
(ImplicationScope (stv 1 1)
   (VariableList
      (TypedVariable
         (Variable "$X")
         (Type "ConceptNode"))
      (TypedVariable
         (Variable "$Y")
         (Type "ConceptNode")))
   (Evaluation
      (Predicate "will-be-friends")
      (List
         (Variable "$X")
         (Variable "$Y")))
   (Evaluation
      (Predicate "will-be-friends")
      (List
         (Variable "$Y")
         (Variable "$X"))))

;; I'm disabling that to simplify the inference. Ultimately the only
;; reason we use will-be-friends rather than are-friends is so the
;; first person perspective makes a bit of sense (cause someone is
;; supposed to know who are her friends). With a third person
;; perspective, such as "Find Sylvia's friends", then we can just use
;; "are-friends", cause we're not supposed to know all of Sylvia's
;; friends.
;;
;; ;; Friends will remain friends.
;; ;;
;; ;; This could simply be expressed as
;; ;;
;; ;; (Implication (stv 0.9 0.9)
;; ;;    (Predicate "are-friends")
;; ;;    (Predicate "will-be-friends"))
;; ;;
;; ;; but due to some current limitation in the type system, specifically
;; ;; that a Predicate cannot be declared with a certain type, we need to
;; ;; express that in a more convoluted way.
;; (ImplicationScope (stv 0.9 0.9)
;;    (VariableList
;;       (TypedVariable
;;          (Variable "$X")
;;          (Type "ConceptNode"))
;;       (TypedVariable
;;          (Variable "$Y")
;;          (Type "ConceptNode")))
;;    (Evaluation
;;       (Predicate "are-friends")
;;       (List
;;          (Variable "$X")
;;          (Variable "$Y")))
;;    (Evaluation
;;       (Predicate "will-be-friends")
;;       (List
;;          (Variable "$X")
;;          (Variable "$Y"))))

;; The probablity of turning acquaintance into friendship between
;; humans is 0.1.
(define human-acquainted-tend-to-become-friends
(ImplicationScope (stv 0.1 0.5)
   (VariableList
      (TypedVariable
         (Variable "$X")
         (Type "ConceptNode"))
      (TypedVariable
         (Variable "$Y")
         (Type "ConceptNode")))
   (And
      (Inheritance
         (Variable "$X")
         (Concept "human"))
      (Inheritance
         (Variable "$Y")
         (Concept "human"))
      (Evaluation
         (Predicate "acquainted")
         (List
            (Variable "$X")
            (Variable "$Y"))))
   (Evaluation
      (Predicate "will-be-friends")
      (List
         (Variable "$X")
         (Variable "$Y")))))

;; Friends tend to be honest
(define friends-tend-to-be-honest
(ImplicationScope (stv 0.85 0.5)
   (VariableList
      (TypedVariable
         (Variable "$X")
         (Type "ConceptNode"))
      (TypedVariable
         (Variable "$Y")
         (Type "ConceptNode")))
   (Evaluation
      (Predicate "will-be-friends")
      (List
         (Variable "$X")
         (Variable "$Y")))
   (And
      (Evaluation
         (Predicate "is-honest")
         (Variable "$X"))
      (Evaluation
         (Predicate "is-honest")
         (Variable "$Y")))))

;;;;;;;;;;;;;;;;;
;; Being Funny ;;
;;;;;;;;;;;;;;;;;

;; Probability of telling a joke to someone. The probability is
;; extremely low because the probability of telling anything to
;; someone is already very low.
(Predicate "told-a-joke-at" (stv 0.000001 0.6))

;; The following should be wrapped in a Lambda and ultimately
;; inferred.
(Evaluation (stv 0.000001 0.6)
   (Predicate "told-a-joke-at")
      (List
         (Variable "$X")
         (Variable "$Y")
         (Variable "$Z")))

;; Probability of being funny
(Predicate "is-funny" (stv 0.69 0.7))

;; Same remark as for Predicate "told-a-joke-at"
(Evaluation (stv 0.69 0.7)
   (Predicate "is-funny")
   (Variable "$X"))

;; People who told a joke to someone, somewhere, are funny  
(define people-telling-jokes-are-funny
(ImplicationScope (stv 0.8 0.9)
   (VariableList
      (TypedVariable
         (Variable "$X")
         (Type "ConceptNode"))
      (TypedVariable
         (Variable "$Y")
         (Type "ConceptNode"))
      (TypedVariable
         (Variable "$Z")
         (Type "ConceptNode")))
   (Evaluation
      (Predicate "told-a-joke-at")
      (List
         (Variable "$X")
         (Variable "$Y")
         (Variable "$Z")))
   (Evaluation
      (Predicate "is-funny")
      (Variable "$X"))))

;; Being funny is loosely equivalent to being amusing
;;
;; This could simply be expressed as
;;
;; (Equivalence (stv 0.7 0.9)
;;    (Predicate "is-funny")
;;    (Predicate "is-amusing"))
;;
;; but due to some current limitation in the type system, specifically
;; that a Predicate cannot be declared with a certain type, we need to
;; express that in a more convoluted way.
(define funny-is-loosely-equivalent-to-amusing
(Equivalence (stv 0.7 0.9)
   (TypedVariable
      (Variable "$X")
      (Type "ConceptNode"))
   (Evaluation
      (Predicate "is-funny")
      (Variable "$X"))
   (Evaluation
      (Predicate "is-amusing")
      (Variable "$X"))))

;;;;;;;;;;;;;;;
;; The Party ;;
;;;;;;;;;;;;;;;

;; Bob told Jill the truth about the party
(Evaluation (stv 1 1)
   (Predicate "told-the-truth-about")
   (List
      (Concept "Bob")
      (Concept "Jill")
      (Concept "Party")))

;; Bob told Jim a joke at the party.
(Evaluation (stv 1 1)
   (Predicate "told-a-joke-at")
      (List
         (Concept "Bob")
         (Concept "Jim")
         (Concept "Party")))

;;;;;;;;;;
;; Hack ;;
;;;;;;;;;;

;; Due to the fact the evaluator does not support fuzzy TV semantic we
;; put the evaluation of a to-be-used instantiated precondition
;; here. Alternatively we could add PLN rules to evaluate.
(define hack (And (stv 1 0.9)
   (Evaluation
      (Predicate "is-honest")
      (Concept "Self")
   )
   (Evaluation
      (Predicate "is-honest")
      (Concept "Bob")
   )
   (Inheritance
      (Concept "Self")
      (Concept "human")
   )
   (Inheritance
      (Concept "Bob")
      (Concept "human")
   )
   (Evaluation
      (Predicate "acquainted")
      (ListLink
         (Concept "Self")
         (Concept "Bob")
      )
   )
)
)

;; Because implication-instantiation occurs on the sugar syntax, the
;; predicate (which should be wrapped in a Lambda) is not given. Also
;; of course that predicate should still be evaluated. Here we provide
;; the adequate TV value of that predicate on the free scope form.
(AndLink (stv 0.000128 0.89999998)
   (EvaluationLink
      (PredicateNode "is-honest")
      (VariableNode "$X")
   )
   (EvaluationLink
      (PredicateNode "is-honest")
      (VariableNode "$Y")
   )
   (InheritanceLink
      (VariableNode "$X")
      (ConceptNode "human")
   )
   (InheritanceLink
      (VariableNode "$Y")
      (ConceptNode "human")
   )
   (EvaluationLink
      (PredicateNode "acquainted")
      (ListLink
         (VariableNode "$X")
         (VariableNode "$Y")
      )
   )
)

Antecedents:

;; People who told the truth about something are honest
(ImplicationScope (stv 0.95 0.9)
  (VariableList
     (TypedVariable
        (Variable "$X")
        (Type "ConceptNode"))
     (TypedVariable
        (Variable "$Y")
        (Type "ConceptNode"))
     (TypedVariable
        (Variable "$Z")
        (Type "ConceptNode")))
  (Evaluation
     (Predicate "told-the-truth-about")
     (List
        (Variable "$X")
        (Variable "$Y")
        (Variable "$Z")))
  (Evaluation
     (Predicate "is-honest")
     (Variable "$X"))))

;; Bob told Jill the truth about the party
(Evaluation (stv 1 1)
  (Predicate "told-the-truth-about")
  (List
     (Concept "Bob")
     (Concept "Jill")
     (Concept "Party")))

Conclusion (1):

(cog-execute! implication-total-instantiation-rule)
;; Bob is honest
   (EvaluationLink (stv 0.94999999 0.89999098)
      (PredicateNode "is-honest" (stv 0.80000001 0.89999998))
      (ConceptNode "Bob")

Antecedent:

;; Friends tend to be honest
(define friends-tend-to-be-honest
(ImplicationScope (stv 0.85 0.5)
  (VariableList
     (TypedVariable
        (Variable "$X")
        (Type "ConceptNode"))
     (TypedVariable
        (Variable "$Y")
        (Type "ConceptNode")))
  (Evaluation
     (Predicate "will-be-friends")
     (List
        (Variable "$X")
        (Variable "$Y")))
  (And
     (Evaluation
        (Predicate "is-honest")
        (Variable "$X"))
     (Evaluation
        (Predicate "is-honest")
        (Variable "$Y")))))

predicate-lambda-introduction-rule:

  Predicate <TV>
  |-
  Lambda <TV>
     <variables>
     Evaluation
        Predicate <TV>
        List
           <variables>

Wrap a Lambda around an evaluation of predicate and assign to the
lambda the TV of the predicate.

Antecedent:

   (LambdaLink
         (VariableList
            (TypedVariableLink
               (VariableNode "$X")
               (TypeNode "ConceptNode")
            )
            (TypedVariableLink
               (VariableNode "$Y")
               (TypeNode "ConceptNode")
            )
         )
         (EvaluationLink
            (PredicateNode "will-be-friends" (stv 9.9999997e-05 0.89999998))
            (ListLink
               (VariableNode "$X")
               (VariableNode "$Y")
            )
         )
      )


Conclusion (3):

   (LambdaLink (stv 9.9999997e-05 0.89999998)
      (VariableList
         (TypedVariableLink
            (VariableNode "$X")
            (TypeNode "ConceptNode")
         )
         (TypedVariableLink
            (VariableNode "$Y")
            (TypeNode "ConceptNode")
         )
      )
      (EvaluationLink
         (PredicateNode "will-be-friends" (stv 9.9999997e-05 0.89999998))
         (ListLink
            (VariableNode "$Y")
            (VariableNode "$X")
         )
      )
   )

predicate-lambda-introduction-rule:

  Predicate <TV>
  |-
  Lambda <TV>
     <variables>
     Evaluation
        Predicate <TV>
        List
           <variables>

Wrap a Lambda around an evaluation of predicate and assign to the
lambda the TV of the predicate.
 

Conclusion (4):
      (LambdaLink (stv 0.63999999 0.89999998)
         (VariableList
            (TypedVariableLink
               (VariableNode "$X")
               (TypeNode "ConceptNode")
            )
            (TypedVariableLink
               (VariableNode "$Y")
               (TypeNode "ConceptNode")
            )
         )
         (AndLink
            (EvaluationLink
               (PredicateNode "is-honest" (stv 0.80000001 0.89999998))
               (VariableNode "$X")
            )
            (EvaluationLink
               (PredicateNode "is-honest" (stv 0.80000001 0.89999998))
               (VariableNode "$Y")
            )
         )
      )

Antecedent:

 ;; people who are friends are more likely to be honest
  (ImplicationLink (stv 0.85000002 0.5)
      (LambdaLink (stv 9.9999997e-05 0.89999998)
         (VariableList
            (TypedVariableLink
               (VariableNode "$X")
               (TypeNode "ConceptNode")
            )
            (TypedVariableLink
               (VariableNode "$Y")
               (TypeNode "ConceptNode")
            )
         )
         (EvaluationLink
            (PredicateNode "will-be-friends" (stv 9.9999997e-05 0.89999998))
            (ListLink
               (VariableNode "$X")
               (VariableNode "$Y")
            )
         )
      )
      (LambdaLink (stv 0.63999999 0.89999998)
         (VariableList
            (TypedVariableLink
               (VariableNode "$X")
               (TypeNode "ConceptNode")
            )
            (TypedVariableLink
               (VariableNode "$Y")
               (TypeNode "ConceptNode")
            )
         )
         (AndLink
            (EvaluationLink
               (PredicateNode "is-honest" (stv 0.80000001 0.89999998))
               (VariableNode "$X")
            )
            (EvaluationLink
               (PredicateNode "is-honest" (stv 0.80000001 0.89999998))
               (VariableNode "$Y")
            )
         )
      )
   )




Conclusion (5):

;; People who are honest are more likely to be friends
   (ImplicationLink (stv 0.00013281251 0.44999999)
      (LambdaLink (stv 0.63999999 0.89999998)
         (VariableList
            (TypedVariableLink
               (VariableNode "$X")
               (TypeNode "ConceptNode")
            )
            (TypedVariableLink
               (VariableNode "$Y")
               (TypeNode "ConceptNode")
            )
         )
         (AndLink
            (EvaluationLink
               (PredicateNode "is-honest" (stv 0.80000001 0.89999998))
               (VariableNode "$X")
            )
            (EvaluationLink
               (PredicateNode "is-honest" (stv 0.80000001 0.89999998))
               (VariableNode "$Y")
            )
         )
      )
      (LambdaLink (stv 9.9999997e-05 0.89999998)
         (VariableList
            (TypedVariableLink
               (VariableNode "$X")
               (TypeNode "ConceptNode")
            )
            (TypedVariableLink
               (VariableNode "$Y")
               (TypeNode "ConceptNode")
            )
         )
         (EvaluationLink
            (PredicateNode "will-be-friends" (stv 9.9999997e-05 0.89999998))
            (ListLink
               (VariableNode "$X")
               (VariableNode "$Y")
            )
         )
      )
   )

 equivalence-to-implication-rule:

  Equivalence
     A
     B
  |-
  Implication
     A
     B
  Implication
     B
     A

Conclusion (13):

;; If X is funny, then X is amusing.
(ImplicationLink (stv 0.82352942 0.89999998)
         (LambdaLink
            (TypedVariableLink
               (VariableNode "$X")
               (TypeNode "ConceptNode")
            )
            (EvaluationLink (stv 0.69 0.69999999)
               (PredicateNode "is-funny" (stv 0.69 0.69999999))
               (VariableNode "$X")
            )
         )
         (LambdaLink
            (TypedVariableLink
               (VariableNode "$X")
               (TypeNode "ConceptNode")
            )
            (EvaluationLink
               (PredicateNode "is-amusing")
               (VariableNode "$X")
            )
         ))

implication-total-instantiation-rule:

 ImplicationScopeLink
     V
     P
     Q
  T
 |-
 Q[V->T]

where V is a variable or a list of variables, P is a condition, Q
is the implicand, T is an atom (or a list of atoms) to substitute
and Q[V->T] is Q where V has been substituted by T.

Conclusion (14):

;;Bob is amusing
(EvaluationLink (stv 0.65882355 0.25109974)
      (PredicateNode "is-amusing")
      (ConceptNode "Bob")
   )

and-introduction-rule:

  A<TV1>
  B<TV2>
  |-
  AndLink <TV>
     A
     B

Conclusion (15):

;; Bob will be an amusing and honest friend.
 (And (stv 0.13281251 0.25109974)
    (Evaluation
       (Predicate "will-be-friends")
       (List
          (Concept "Self")
          (Concept "Bob")))
    (Evaluation
       (Predicate "is-amusing")
       (Concept "Bob"))
    (Evaluation
       (Predicate "is-honest")
       (Concept "Bob")))