;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
;%%% ALC algorithm and others %
;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
;%%% %
;%%% Umberto Straccia %
;%%% http://faure.iei.pi.cnr.it/~straccia %
;%%% straccia@iei.pi.cnr.it %
;%%% %
;%%% Adapted by Antonio Lopreiato %
;%%% May 5th 1998 %
;%%% %
;%%% Version 0.0 %
;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The system presents a list of functionalities about the ALC language.
The system is a very naive implementation.

;;The language contains letters (denoted by P,Q)
;;and assertions 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
;;
;; 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)}
;;
;;R,C,a,b -> (*isc* a C) ;concept assertion
;; | (*isr* (a b) R) ;role assertion
;; | (*axm* AX) ;axiom


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

;;---------------------------------------------------------------------------
;; alc-sat (p)
;; Input: ALC assertion
;; Return: result = true if SAT fp
;;---------------------------------------------------------------------------

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

;;---------------------------------------------------------------------------
;; alc-logically-implies (KB p)
;; Input: KB = list of ALC assertions
;; fp = an ALC assertion
;; Return: result = true if KB |= fp
;;---------------------------------------------------------------------------

;;---------------------------------------------------------------------------
;; alc-logically-implies-ext (ext-KB q)
;; Input: ext-KB = list of completions (see below for more info)
;; q = an ALC assertion (the query)
;; Return: result = true if ext-KB |= q
;;---------------------------------------------------------------------------

;;---------------------------------------------------------------------------
;; alc-tautology (p)
;; Input: fp = an ALC assertion
;; Return: result = true if |= fp
;;---------------------------------------------------------------------------

;;---------------------------------------------------------------------------
;; alc-get-a-model (p)
;; Input: an ALC proposition
;; Return: both a list of ALC primitive (positive) concepts and roles
;; i.e. an Herbrand model of p, or (NIL) that is the empty model.
;; Return nil if no models are avalaible
;;---------------------------------------------------------------------------

;;---------------------------------------------------------------------------
;; alc-KB-get-a-model (KB)
;; Input: a list of ALC propositions
;; Return: both a list of ALC primitive (positive) concepts and roles
;; i.e. an Herbrand model of KB, or (NIL) that is the empty model.
;; Return nil if no models are avalaible
;;---------------------------------------------------------------------------

;;---------------------------------------------------------------------------
;; alc-get-all-models (p)
;; Input: an ALC proposition
;; Return: both a list of ALC primitive (positive) concepts and roles
;; i.e. an Herbrand model of fp, or (NIL) that is the empty model.
;; Return nil if no models are avalaible
;;---------------------------------------------------------------------------

;;---------------------------------------------------------------------------
;; alc-KB-get-all-models (KB)
;; Input: a list of ALC propositions
;; Return: both a list of ALC primitive (positive) concepts and roles
;; i.e. an Herbrand model of KB, or (NIL) that is the empty model.
;; Return nil if no models are avalaible
;;---------------------------------------------------------------------------

;;---------------------------------------------------------------------------
;; alc-get-a-completion (p)
;; Input: an ALC proposition
;; Return: both a list of ALC primitive (positive) concepts, roles,
;; 'ALL' concepts and axioms, i.e. an Herbrand model of p,
;; or (NIL) that is the empty model.
;; Return nil if no models are avalaible
;;---------------------------------------------------------------------------

;;---------------------------------------------------------------------------
;; alc-KB-get-a-completion (KB)
;; Input: a list of ALC propositions
;; Return: both a list of ALC primitive (positive) concepts, roles,
;; 'ALL' concepts and axioms, i.e. an Herbrand model of p,
;; or (NIL) that is the empty model.
;; Return nil if no models are avalaible
;;---------------------------------------------------------------------------

;;---------------------------------------------------------------------------
;; alc-get-all-completions (p)
;; Input: an ALC proposition
;; Return: both a list of ALC primitive (positive) concepts, roles,
;; 'ALL' concepts and axioms, i.e. an Herbrand model of p,
;; or (NIL) that is the empty model.
;; Return nil if no models are avalaible
;;---------------------------------------------------------------------------

;;---------------------------------------------------------------------------
;; alc-KB-get-all-completions (KB)
;; Input: a list of ALC propositions
;; Return: both a list of ALC primitive (positive) concepts, roles,
;; 'ALL' concepts and axioms, i.e. an Herbrand model of p,
;; or (NIL) that is the empty model.
;; Return nil if no models are avalaible
;;---------------------------------------------------------------------------


Moreover, it contains an automatic ALC assertional formulae generator, and
statistical ALC testing code.

VERY IMPORTANT NOTE:
====================

The calculus is complete iff:

1.KB's axioms are cycles-free.
A set of axioms is cycles-free if its transitive closure has
no elements such that axiom's head is contained into axiom's body.

2.Let AXS be 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