#|
Reasoning capabilities:
-----------------------

 * Unsatisfiability. You break a rule
  e.g. You have defined two classes that are disjoint, and a third class is the intersection of those two classes.  Third class is unsatisfiable.
  and Inconsistency:    
  e.g. An instance is a member of two classes that are disjoint.  
  Fact claiming Instance is member of both classes is inconsistent.

 * Classification:  
 * Realization: finding types of an instance.
 * Inferring additional relations based on properties.

 Understanding different aspects of properties:

 * Transitive A rel B and B rel C implies A rel C
 * Functional:  A rel B and A rel C implies B == C
 * Inverse Functional:   A rel B and C rel B implies A == C
 * Symmetric:  A rel B implies B rel A

|#


(define-ontology simple-class-hierarchy () 
  (class !A :partial) 
  (class !B :partial) 
  (class !C :partial) 
  (sub-class-of !B !A) 
  (sub-class-of !C !B)  
  )
(describe-entity !C (kb simple-class-hierarchy))


;; We want to infer (sub-class !C !A)

(define-ontology inconsistent-ontology (:base "http://www.example.com" )
  (class !A :partial)
  (class !B :partial)
  (disjoint-classes !A !B)
  (individual !an-a-and-b (type !A) (type !B)))

(check inconsistent-ontology)

(with-ontology unsatisfiable-ontology ()
  ((class !A :partial)
   (individual !a (type !A))
   (class !B :partial)
   (disjoint-classes !A !B)
   (class !C :complete (intersection-of !A !B)))
  (assert (member !C (unsatisfiable-classes unsatisfiable-ontology) ) () "!C should be unsatisfiable"))


(define-ontology transitive-property ()
  (object-property !P :transitive)
  (class !A :partial)
  (individual !a1 (type !A) (value !P !a2))
  (individual !a2 (type !A) (value !P !a3))
  (individual !a3 (type !A)))

(setq *default-kb* (kb transitive-property))
(describe-entity (uri-full !a1))
#|
Individual http://example.com/#a1
All Types: ex:A
Direct Types: ex:A
ex:P: "ex:a3", "ex:a2"
|#

(define-ontology two-value-inconsistency ()
  (object-property !gender)
  (class !human :partial (restriction !gender (cardinality 1)))
  (individual !male)
  (individual !female)
  (different-individuals !male !female)
  (individual !transgender (type !human)
	      (value !gender !male)
	      (value !gender !female)))
(check two-value-inconsistency)
;; !transgender is inconsistent

(define-ontology republican-ontology ()
  (class !Hippie :partial)
  (class !Suit :partial)
  (disjoint-classes !Hippie !Suit)
  (individual !abbie-hoffman (type !Hippie))
  (individual !dick-cheney (type !Suit))
  (object-property !exclusive-member (range !Suit))
  (class !Republican-party :partial)
  (individual !republican-national-convention (type !Republican-party) 
	      (value !exclusive-member !abbie-hoffman)))

(check republican-ontology)

(define-ontology wrong-class ()
  (class !Hippie :partial)
  (class !Suit :partial)
  (disjoint-classes !Hippie !Suit)
  (individual !abbie-hoffman (type !Hippie))
  (individual !dick-cheney (type !Suit))
  (object-property !exclusive-member)
  (class !Republican-party :partial (restriction !exclusive-member (all-values-from !Suit)))
  (individual !republican-national-convention (type !Republican-party) 
	      (value !exclusive-member !abbie-hoffman)))

(check wrong-class)

(define-ontology wrong-value ()
  (class !flavor :partial)
  (individual !chocolate (type !flavor))
  (individual !vanilla (type !flavor))
  (different-individuals !chocolate !vanilla)
  (object-property !has-flavor)
  (class !ice-cream :complete (restriction !has-flavor (has-value !chocolate))
	 (restriction !has-flavor (cardinality 1)))
  (individual !my-ice-cream (type !ice-cream) (value !has-flavor !vanilla)))

(check wrong-value)