;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
;%%% Fuzzy ALC algorithm and others 				             %
;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
;%%% 									     %
;%%% Umberto Straccia 							     % 
;%%% http://faure.iei.pi.cnr.it/~straccia				     %
;%%% straccia@iei.pi.cnr.it 						     % 
;%%% 									     % 
;%%% Adapted by Antonio Lopreiato                                            %
;%%% September 10th 1998                                                     % 
;%%%   									     %
;%%% Version 1.0                                                             %
;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The system presents a list of functionalities about a fuzzy description logic.
The system is a very naive implementation.

;;The language contains letters (primitive concepts, denoted by P,Q) 
;;and concepts denoted by (C,D) which are built 
;;according to the following rule:
;;
;;C,D -> P              ;letter
;;     | *top*          ;true
;;     | *bot*          ;false
;;     | (not P)        ;negation
;;     | (and C D ...)  ;conjunction
;;     | (or C D ...)   ;disjunction
;;     | (all R C)      ;universal quantifier
;;     | (csome R C)    ;existential quantifier
;;
;;  R -> Q              ; role identifier
;;
;; AX -> (if P C)       ;primitive concept P implies C
;;     | (onlyif P C)   ;concept C implies P
;;     | (iff P C)      ;equivalent to the set {(if P C),(onlyif P C)}
;;
;;ASS -> (*isc* a C)      ;concept assertion
;;     | (*isr* (a b) R)  ;role assertion
;;   
;; AF -> (ASS RELOP n)        ;fuzzy (af-)assertion, 0<= n <=1
;;     | ((*axm* AX))         ;axiom assertion 
;;
;; RELOP -> >= | <=                                

FUNCTIONS:
==========

;;--------------------------------------------------------------------------- 
;; af-sat (af)
;; Input: ALC fuzzy assertion 
;; Return: result = true if SAT af
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; af-sat-KB (af-list)
;; Input: list of ALC fuzzy assertions, i.e. a KB 
;; Return: result = true if SAT af-list
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; af-logically-implies (kb af)
;; Input: kb = list of ALC fuzzy assertions, i.e. a KB 
;;        af  = a fuzzy ALC assertion
;; Return: result = true if KB |= af
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; af-logically-implies-ext (ext-kb af)
;; Input: ext-kb = a list of af-completions
;;        af  = a fuzzy ALC assertion
;; Return: result = true if ext-kb |= af
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; af-tautology (af)
;; Input: af  = a fuzzy ALC assertion
;; Return: result = true if |= af
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; af-get-a-completion (af)
;; Input: ALC fuzzy assertion 
;; Return: both a list of ALC primitive concepts, roles, 
;;         'ALL' concepts and axioms in the form of saf-assertions.
;;         The form (NIL) stands for the empty completion. 
;;         Return nil if no completions are avalaible
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; af-KB-get-a-completion (af-list)
;; Input: a list of ALC fuzzy assertions
;; Return: both a list of ALC primitive concepts, roles, 
;;         'ALL' concepts and axioms in the form of saf-assertions.
;;         The form (NIL) stands for the empty completion. 
;;         Return nil if no completions are avalaible
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; af-get-all-completion (af)
;; Input: ALC fuzzy assertion 
;; Return: both a list of ALC primitive (positive) concepts, roles, 
;;         'ALL' concepts and axioms in the form of saf-assertions.
;;         The form (NIL) stands for the empty completion. 
;;         Return nil if no completions are avalaible
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; af-KB-get-all-completions (af-list)
;; Input: a list of ALC fuzzy assertions 
;; Return: both a list of ALC primitive concepts, roles, 
;;         'ALL' concepts and axioms in the form of saf-assertions.
;;         The form (NIL) stands for the empty completion. 
;;         Return nil if no completions are avalaible
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; cs-KB-get-all-completions (kb)
;; Input: a list of ALC fuzzy assertions 
;; Return: both a list of ALC primitive concepts, roles, 
;;         'ALL' concepts and axioms in the form of cs-assertions.
;;         The form (NIL) stands for the empty completion. 
;;         Return nil if no completions are avalaible
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; af-get-a-model (af)
;; Input: ALC fuzzy assertion 
;; Return: a list of weighted primitive concepts and roles,
;;         i.e. a fuzzy Herbrand model of fp.
;;         The form (NIL) stands for the empty model. 
;;         Return nil if no models are avalaible
;;---------------------------------------------------------------------------

;;--------------------------------------------------------------------------- 
;; af-KB-get-a-model (af-list)
;; Input: a list of ALC fuzzy assertions
;; Return: a list of weighted primitive concepts and roles,
;;         i.e. a fuzzy Herbrand model of fp.
;;         The form (NIL) stands for the empty model. 
;;         Return nil if no models are avalaible
;;---------------------------------------------------------------------------

;;--------------------------------------------------------------------------- 
;; af-get-all-models (af)
;; Input: ALC fuzzy assertion 
;; Return: a list of weighted primitive concepts and roles,
;;         i.e. a fuzzy Herbrand model of fp.
;;         The form (NIL) stands for the empty model. 
;;         Return nil if no models are avalaible
;;---------------------------------------------------------------------------

;;--------------------------------------------------------------------------- 
;; af-KB-get-all-models (af-list)
;; Input: a list of ALC fuzzy assertions 
;; Return: a list of weighted primitive concepts and roles,
;;         i.e. a fuzzy Herbrand model of fp.
;;         The form (NIL) stands for the empty model. 
;;         Return nil if no models are avalaible
;;---------------------------------------------------------------------------

;;--------------------------------------------------------------------------- 
;; af-glb (kb af)
;; Input: kb = list of fuzzy ALC assertions, i.e. a KB 
;;        af  = an ALC assertion
;; Return: af's greatest lower bound given kb, that is
;;         {max n | n belongs to (0 1] and kb |= (af >= n)}; 
;;         return 0 if such n does'nt exist ;;
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; af-lub (kb af)
;; Input: kb = list of fuzzy ALC assertions, i.e. a KB 
;;        af  = an ALC assertion
;; Return: af's lowest upper bound given kb, that is
;;         {min n | n belongs to [0 1) and kb |= (af <= n)}; 
;;         return 1 if such n does'nt exist ;;
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; ext-af-glb (ext-kb af)
;; Input: ext-kb = list of cs-completions
;;        af  = an ALC assertion
;; Return: af's greatest lower bound given ext-kb, that is
;;         {max n | n belongs to (0 1] and kb |= (af >= n),
;;                  for each kb in ext-kb}; 
;;         return 0 if such n does'nt exist ;;
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; ext-af-lub (ext-kb af)
;; Input: ext-kb = list of cs-completions, i.e. a list of KBs 
;;        af  = an ALC assertion
;; Return: af's lower upper bound given ext-kb, that is
;;         {min n | n belongs to [0 1) and kb |= (af <= n),
;;                  for each kb in ext-kb}; 
;;         return 1 if such n does'nt exist  
;;--------------------------------------------------------------------------- 


Moreover, it contains an automatic fuzzy assertions generator, and 
statistical ALC-F testing code.

NOTE:
=====

Many other functions can be easily realized, as the system is very modular.

It is based on a trivial search algorithm in a space of states. 
Each state encodes a problem to be solved.
It starts with a set of states to be solved
and returns true if all of them can be solved.

;; In order to execute the hole procedure, you should define

1. The structure of a state
2. a function get-new-states:State-->2^S, which given the current state,
generates the next state to be analysed
3. a function closed-state:State-->{true,false}, which given a state say
whether it is closed (i.e. solved)
4. a function termination-case, which says whether the search should be
stopped
5. a function get-result, which returns the result of the search 

Therefore, any deduction system can be easily implemented.

The main search procedure returns:

;; (result lopen-states lclosed-states l-completed-states current-state lintermediate-states)
;; 1. result ; = true problem is solved
;; 2. lopen-states ; list of to be solved states
;; 3. lclosed-states ; list of solved states
;; 4. lcompleted-states ; list of completed states, but not solved
;; 5. current-state ; current state in which the search has been stopped
;; 6. lintermediate-states ; list of all other states processed

;;--------------------------------------------------------------------------- 

If you have questions or any other suggestions, don't hesitate to contact me.

straccia@iei.pi.cnr.it 
