[Javaowl-commit] reasoner/design ALC-Reasoner.scm,NONE,1.1 draft.scm,1.8,1.9

[Gerardo H. <ma...@us...>]

Update of /cvsroot/javaowl/reasoner/design
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv27294

Modified Files:
	draft.scm 
Added Files:
	ALC-Reasoner.scm 
Log Message:
Added generalized existential quantifier.


Index: draft.scm
===================================================================
RCS file: /cvsroot/javaowl/reasoner/design/draft.scm,v
retrieving revision 1.8
retrieving revision 1.9
diff -C2 -d -r1.8 -r1.9
*** draft.scm	8 Aug 2004 05:32:53 -0000	1.8
--- draft.scm	14 Aug 2004 18:39:53 -0000	1.9
***************
*** 64,65 ****
--- 64,76 ----
    '((Parent Gerardo)
      (Childless Gerardo)))
+ 
+ (define tbox7
+   '(($= Woman ($intersection Person Female))
+     ($= Man ($intersection Person ($complement Female)))
+     ($= Childless ($allValuesFrom hasChild $BOTTOM))
+     ($= Parent ($someValuesFrom hasChild $TOP))))
+ 
+ (define abox7
+   '((Parent Gerardo)
+     (Childless Gerardo)))
+ 

--- NEW FILE: ALC-Reasoner.scm ---
(require 'list-lib)

(define (find-definition tbox predicate)
  (if (null? tbox)
      #f
      (if (predicate (car tbox))
          (car tbox)
          (find-definition (cdr tbox) predicate))))

(define (definition? tbox-term)
  (equal? (first tbox-term) '$=))

(define (concept-definition? tbox-term concept)
  (and (definition? tbox-term)
       (equal? (second tbox-term) concept)))

(define (get-concept-definition tbox concept)
  (let ((tbox-term (find-definition tbox (lambda (x) (concept-definition? x concept)))))
    (if tbox-term (third tbox-term) #f)))

(define (replace-concept-definition tbox concept new-definition)
  (if (null? tbox)
      ()
      (let ((tbox-term (car tbox))
            (tbox-terms (cdr tbox)))
        (if (concept-definition? tbox-term concept)
            (cons `($= ,concept ,new-definition) tbox-terms)
            (cons tbox-term
                  (replace-concept-definition tbox-terms concept new-definition))))))

(define (complement concept)
  (letrec
      ((complement-intersection
        (lambda (concepts)
          `($union ,@(map (lambda (x) (complement x)) concepts))))

       (complement-union
        (lambda (concepts)
          `($intersection ,@(map (lambda (x) (complement x)) concepts))))

       (complement-allValuesFrom
        (lambda (role-concept)
          (let ((role (first role-concept))
                (concept (second role-concept)))
            `($someValuesFrom ,role ,(complement concept)))))

       (complement-someValuesFrom
        (lambda (role-concept)
          (let ((role (first role-concept))
                (concept (second role-concept)))
            `($allValuesFrom ,role ,(complement concept)))))

       (complement-complement
        (lambda (concepts)
          (first concepts))))
    
    (if (symbol? concept)
        `($complement ,concept)
        (let ((constr (car concept))
              (concepts (cdr concept)))
          (cond ((eq? constr '$intersection) (complement-intersection concepts))
                ((eq? constr '$union) (complement-union concepts))
                ((eq? constr '$allValuesFrom) (complement-allValuesFrom concepts))
                ((eq? constr '$someValuesFrom) (complement-someValuesFrom concepts))
                ((eq? constr '$complement) (complement-complement concepts))
                (#t (error "unexpected constructor: " constr)))))))
                                              
(define (simplify definition)
  (letrec
      ((simplify-complement
        (lambda (concepts)
         (let ((concept (first concepts)))
           (if (symbol? concept)
               `($complement ,concept)
               (simplify (complement concept))))))

       (flatten-intersection
        (lambda (concepts)
          (if (null? concepts)
              ()
              (let ((concept (car concepts))
                    (other-concepts (cdr concepts)))
                (if (and (pair? concept)
                         (eq? (first concept) '$intersection))
                    (append (cdr concept) (flatten-intersection other-concepts))
                    (cons concept (flatten-intersection other-concepts)))))))

       (reduce-intersection
        (lambda (concepts)
          (cond ((memq '$BOTTOM concepts) '($BOTTOM))
                ((null? concepts) ())
                (#t (let ((concept (car concepts))
                          (other-concepts (cdr concepts)))
                      (if (or (eq? concept '$TOP)
                              (member concept other-concepts))
                          (reduce-intersection other-concepts)
                          (cons concept (reduce-intersection other-concepts))))))))

       (check-unary-intersection
        (lambda (concepts)
          (if (= (length concepts) 1)
              (first concepts)
              `($intersection ,@concepts))))

       (simplify-intersection
        (lambda (concepts)
          (check-unary-intersection (reduce-intersection (flatten-intersection (map simplify concepts))))))

       (flatten-union
        (lambda (concepts)
          (if (null? concepts)
              ()
              (let ((concept (car concepts))
                    (other-concepts (cdr concepts)))
                (if (and (pair? concept)
                         (eq? (first concept) '$union))
                    (append (cdr concept) (flatten-union other-concepts))
                    (cons concept (flatten-union other-concepts)))))))

       (reduce-union
        (lambda (concepts)
          (cond ((memq '$TOP concepts) '($TOP))
                ((null? concepts) ())
                (#t (let ((concept (car concepts))
                          (other-concepts (cdr concepts)))
                      (if (or (eq? concept '$BOTTOM)
                              (member concept other-concepts))
                          (reduce-union other-concepts)
                          (cons concept (reduce-union other-concepts))))))))

       (check-unary-union
        (lambda (concepts)
          (if (= (length concepts) 1)
              (first concepts)
              `($union ,@concepts))))

       (simplify-union
        (lambda (concepts)
          (check-unary-union (reduce-union (flatten-union (map simplify concepts))))))

       (simplify-allValuesFrom
        (lambda (concepts)
          (let ((sarg (simplify (second concepts)))
                (role (first concepts)))
            (cond ((and (pair? sarg)
                        (eq? (first sarg) '$intersection))
                   `($intersection ,@(map (lambda (x) `($allValuesFrom ,role , x)) (cdr sarg))))
                  ((and (pair? sarg)
                        (eq? (first sarg) '$union))
                   `($union ,@(map (lambda (x) `($allValuesFrom ,role , x)) (cdr sarg))))
                  ((eq? sarg '$TOP) '$TOP)
                  (#t `($allValuesFrom ,role ,sarg))))))

       (simplify-someValuesFrom
        (lambda (concepts)
          (let ((role (first concepts))
                (sarg (simplify (second concepts))))
            `($someValuesFrom ,role ,sarg)))))
    
    (if (symbol? definition)
        definition
        (let ((constr (car definition))
              (concepts (cdr definition)))
          (cond ((eq? constr '$intersection) (simplify-intersection concepts))
                ((eq? constr '$union) (simplify-union concepts))
                ((eq? constr '$allValuesFrom) (simplify-allValuesFrom concepts))
                ((eq? constr '$complement) (simplify-complement concepts))
                ((eq? constr '$someValuesFrom) (simplify-someValuesFrom concepts))
                (#t (error "unexpected constructor: " constr)))))))
      
(define (expand-concept-definition tbox definition)
  (if (symbol? definition)
      (let ((expansion (get-concept-definition tbox definition)))
        (if expansion
            (expand-concept-definition tbox expansion)
            definition))
      (cons (car definition)
            (map (lambda (x) (expand-concept-definition tbox x)) (cdr definition)))))

(define (expand-tbox tbox)
  (letrec
      ((rec-expand-tbox
        (lambda (tbox exp-tbox)
          (if (null? tbox)
              exp-tbox
              (let ((tbox-term (car tbox))
                    (tbox-terms (cdr tbox)))
                (if (definition? tbox-term)
                    (let* ((concept (second tbox-term))
                           (definition (third tbox-term))
                           (new-exp-tbox
                            (replace-concept-definition exp-tbox concept
                                                        (simplify (expand-concept-definition exp-tbox
                                                                                             definition)))))
                      (rec-expand-tbox tbox-terms new-exp-tbox))
                    (cons tbox-term (rec-expand-tbox tbox-terms exp-tbox))))))))
    (cons '($= $BOTTOM ($complement $TOP)) (rec-expand-tbox tbox tbox))))

(define (apply-rules abox)
  (letrec
      ((apply-intersection
        (lambda (concepts instance r-abox)
          (if (null? concepts)
              r-abox
              (let* ((concept (car concepts))
                     (other-concepts (cdr concepts))
                     (term `(,concept ,instance)))
                (apply-intersection other-concepts instance (if (member term r-abox)
                                                                r-abox
                                                                (apply-rules (cons term r-abox))))))))
       (check-allValuesFrom
        (lambda (instances concept r-abox)
          (if (null? instances)
              r-abox
              (let* ((instance (car instances))
                     (other-instances (cdr instances))
                     (term `(,concept ,instance)))
                (check-allValuesFrom other-instances concept (if (member term r-abox)
                                                                 r-abox
                                                                 (apply-rules (cons term r-abox))))))))
       
       (apply-allValuesFrom
        (lambda (role-concept instance r-abox)
          (let ((role (first role-concept))
                (concept (second role-concept)))
            (check-allValuesFrom (map third (filter (lambda (x) (and (equal? role (first x))
                                                                     (equal? instance (second x)))) r-abox))
                                 concept r-abox))))

       (some-values-from?
        (lambda (instances concept r-abox)
          (> (length (filter (lambda (x) (member `(,concept ,x) r-abox)) instances)) 0)))

       (apply-someValuesFrom
        (lambda (role-concept instance r-abox)
          (let* ((role (first role-concept))
                 (concept (second role-concept))
                 (roles (filter (lambda (x) (and (equal? role (first x))
                                                (equal? instance (second x)))) r-abox)))
            (if (not (some-values-from? (map third roles) concept r-abox))
                (let ((tmp (gentemp)))
                  (apply-rules `((,concept ,tmp) (,role ,instance ,tmp) ,@r-abox)))
                r-abox))))
        
        (apply-concept
         (lambda (concept instance r-abox)
           (if (not (eq? concept '$TOP))
               (let ((term `($TOP ,instance)))
                 (if (member term r-abox)
                     r-abox
                     (cons term r-abox)))
               r-abox)))
       
       (rec-apply-rules
        (lambda (abox r-abox)
          (if (null? abox)
              r-abox
              (let* ((term (car abox))
                     (concept (first term))
                     (instance (second term))
                     (terms (cdr abox)))
                (cond ((symbol? concept)
                       (if (= (length term) 3)
                           (rec-apply-rules terms r-abox)
                           (rec-apply-rules terms (apply-concept concept instance r-abox))))
                      ((eq? (car concept) '$intersection)
                       (rec-apply-rules terms (apply-intersection (cdr concept) instance r-abox)))
                      ((eq? (car concept) '$allValuesFrom)
                       (rec-apply-rules terms (apply-allValuesFrom (cdr concept) instance r-abox)))
                      ((eq? (car concept) '$someValuesFrom)
                       (rec-apply-rules terms (apply-someValuesFrom (cdr concept) instance r-abox)))
                      (#t (rec-apply-rules terms (apply-concept concept instance r-abox)))))))))
    (rec-apply-rules abox abox)))

(define (has-contradiction? abox)
  (letrec
      ((complement
        (lambda (t)
          (let ((concept (first t))
                (instance (second t)))
            (cond ((symbol? concept) `(($complement ,concept) ,instance))
                  (#t `(,(second concept) ,instance))))))
       (base-concept?
        (lambda (c)
          (or (symbol? c)
              (eq? (first c) '$complement)))))

    (if (null? abox)
        #f
        (let ((term (car abox))
              (terms (cdr abox)))
          (if (= (length term) 3)
              (has-contradiction? terms)
              (if (and (base-concept? (first term))
                       (member (complement term) terms))
                  #t
                  (has-contradiction? terms)))))))

(define (consistent? abox)
  (not (has-contradiction? (apply-rules abox))))

(define (expand-wrt-tbox abox tbox)
  (letrec
      ((etbox (expand-tbox tbox))

       (rec-expand-wrt-tbox
        (lambda (abox eabox)
          (if (null? abox)
              eabox
              (let ((term (car abox))
                    (other-terms (cdr abox)))
                (if (= (length term) 2)
                    (rec-expand-wrt-tbox other-terms
                                         (cons `(,(simplify (expand-concept-definition etbox (first term)))
                                                 ,(second term))
                                               eabox))
                    (rec-expand-wrt-tbox other-terms (cons term eabox))))))))

    (rec-expand-wrt-tbox abox ())))

(define (consistent-wrt-tbox? abox tbox)
  (consistent? (expand-wrt-tbox abox tbox)))