;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
;%%% 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