;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
;%%% 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.
VERY IMPORTANT NOTE:
====================
The calculus is complete iff:
1.KB's axioms are cycle-free.
A set of axioms is cycles-free if its transitive closure contains
no elements such that axiom's head is contained into axiom's body.
2.Let AXS the set of KB's axioms simplified in the form (if A C), (onlyif A C).
For all pairs of axioms (if P D), (onlyif P E) in AXS, with identical head P,
D = E should hold.
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