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

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 models of p
;;---------------------------------------------------------------------------

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

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