;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
;%%% Fuzzy Sat 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 fuzzy logic.
The system is a very naive implementation.

;;The language contains letters (denoted by P) 
;;and propositions denoted by (A,B) which are built 
;;according to the following rules:
;;
;;A,B -> P ;letter
;; | *top* ;true
;; | *bot* ;false
;; | (not A) ;negation
;; | (and A B ...) ;conjunction
;; | (or A B ...) ;disjunction
;;
;;A fuzzy formula is built according to the following rule:
;;
;;F -> (A n) where n is a real number belonging to the interval (0,1]
;;           and A is a proposition

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

;;--------------------------------------------------------------------------- 
;; fp-sat (fp)
;; Input: fuzzy proposition 
;; Return: result = true if SAT fp
;;--------------------------------------------------------------------------- 

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

;;--------------------------------------------------------------------------- 
;; fp-logically-implies (fkb fp)
;; Input: fkb = list of fuzzy propositions, i.e. a KB 
;;        fp  = a fuzzy proposition
;; Return: result = true if KB |= fp
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; fp-tautology (fp)
;; Input: fp  = a fuzzy proposition
;; Return: result = true if |= fp
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; fp-get-a-model (p)
;; Input: a fuzzy proposition 
;; Return: a list of weighted literals in the form (A d) or ((NOT A) d).
;;         (A d) [resp. ((not A) d)] stand for (A >= d) [resp. ((not A) >= d)].
;;         In the two-values calculus literals of form ((not A) >= d)
;;         are equivalent to (A <= (1-d)).
;;         Return nil if no models are avalaible
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; fp-KB-get-a-model (fp-list)
;; Input: a list of fuzzy propositions 
;; Return: a list of weighted literals in the form (A d) or ((NOT A) d).
;;         (A d) [resp. ((not A) d)] stand for (A >= d) [resp. ((not A) >= d)].
;;         In the two-values calculus literals of form ((not A) >= d)
;;         are equivalent to (A <= (1-d)).
;;         Return nil if no models are avalaible
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; fp-get-all-models (fp)
;; Input: a fuzzy proposition 
;; Return: a list of weighted literals in the form (A d) or ((NOT A) d).
;;         (A d) [resp. ((not A) d)] stand for (A >= d) [resp. ((not A) >= d)].
;;         In the two-values calculus literals of form ((not A) >= d)
;;         are equivalent to (A <= (1-d)).
;;         Return nil if no models are avalaible
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; fp-KB-get-all-models (fp-list)
;; Input: a list of fuzzy propositions 
;; Return: a list of weighted literals in the form (A d) or ((NOT A) d).
;;         (A d) [resp. ((not A) d)] stand for (A >= d) [resp. ((not A) >= d)].
;;         In the two-values calculus literals of form ((not A) >= d)
;;         are equivalent to (A <= (1-d)).
;;         Return nil if no models are avalaible
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; fp-maxDegree (fkb p)
;; Input: fkb = list of fuzzy propositions, i.e. a KB 
;;        p  = a proposition
;; Return: the max n belonging to real interval (0,1] such that KB |= (p n),
;;         or 0 if there is no such n 
;;--------------------------------------------------------------------------- 

Moreover, it contains an automatic fuzzy propositional formulae generator, and 
statistical SAT-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 