;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
;%%% Sat algorithm and others                                                %
;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%                                                                        %
;%%%                                                                         %
;%%% Umberto Straccia                                                        %                                                
;%%% http://faure.iei.pi.cnr.it/~straccia                                    %
;%%% straccia@iei.pi.cnr.it                                                  %                                                
;%%%                                                                         % 
;%%% October, 6th 1997                                                       %
;%%%                                                                         %
;%%% Version 0.0                                                             %
;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The system presents a list of functionalities about propositional 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 rule:
;;
;;A,B -> P              ;letter
;;     | *top*          ;true
;;     | *bot*          ;false
;;     | (not A)        ;negation
;;     | (and A B ...)  ;conjunction
;;     | (or A B ...)   ;disjunction
;;     | (if A B)       ;implication
;;     | (iff A B)      ;if and only if


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

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

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

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

;;--------------------------------------------------------------------------- 
;; p-get-a-model (p)
;; Input: proposition 
;; Return: a list of letters = a Herbrand model of p, nil otherwise
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; p-KB-get-a-model (p-list)
;; Input: a list of propositions, i.e. a KB
;; Return: a list of letters = a Herbrand model of the KB, nil otherwise
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; p-get-all-models (p)
;; Input: proposition 
;; Return: a list of all Herbrand model of p, nil otherwise
;;--------------------------------------------------------------------------- 

;;--------------------------------------------------------------------------- 
;; p-KB-get-all-models (p-list)
;; Input: a list of propositions 
;; Return: a list of all Herbrand model of p-list, nil otherwise
;;--------------------------------------------------------------------------- 

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

