Clojure, tautology and logical expression

Introduction
I decided to create a simple Clojure project for verifying logical tautologies. The source code is available here.

For instance:


The algorithm is simple:

1. Parse the logical expression
2. Generate all possible combination of values for literals in the expression
3. Evaluate the results for any value
4. If every result is true then we have a tautology
   

It is not an optimal method for proving the tautology because the complexity is exponential but if we have a small number of literals it can run pretty fast.

Definition
Grammar for logical expression to be analyzed:

<expression> ::=
    [~] < expression >
         | <literal>
         | ( < expression > <operator> <expression>)

< literal > ::= chain of letter and digits starting from letter
< operator > ::= 
    & : logical AND
    ^ : logical OR
    == : logical equivalence
    => : logical implication
    ~ : logical NOT

Remarks:

• I assume that every subexpression (except literals) should be enclosed in parenthesis. For instance: (A & B) but not (A & B ^ C). This I'm avoiding a problem related to operator precedence. Because any logical expression can be "normalized" that way it is not a limitation which matters.
• The tautology quoted above can be put down that way: (( A & B) => C) == (A => (B => C))
• One of De Morgan's Laws: ~(A & B) == (~A ^ ~B)

Parser
The first thing to do is the "tokenizer" - creates a flow of separated components. It can be achieved simply by means of regular expression.

  [seqw (re-seq #"[A-Za-z][\w]*|[\^\(\)&~]|=>|==" str)]

Source code for parser is available here.

 
defn parse
"parse string expression
 returns three element vector (Polish notation: (operator, left operand, right operand)
 left/right operand can be an atomic operand (variable) or 
 subexpression (another triada vector)"
[str]

Parser decomposes input string to "Polish notation". Every part of the expression is transformed to a triad [operator, left operand, right operand]. In the case of negation (one parameter operator) the right operand is nil.

Evaluation

The evaluation (counting value) is very simple while the expression is decomposed.

(defn evaluate 
    [expr val]

"evaluate (calculate value) of the parsed expression using current values (as hash-map)
 returns true or false
"
    (defn getval [subexpr]
    (let 
      [operator (first subexpr)
       first (fnext subexpr)
       second (nth subexpr 2)
       firstval (if (vector? first) (getval first) (get val first))
       secondval (if (vector? second) (getval second) (get val second))
      ] 
     (cond 
        (= operator nil) firstval
        (= operator "&") (and firstval secondval)
        (= operator "^") (or firstval secondval)
        (= operator "==") (= firstval secondval)
        (= operator "=>") (if (and firstval (not secondval)) false true)
        (= operator "~") (not firstval)
        :else nil
     )
     )
     )
     (getval expr)
)

Just scan the parsed expression and calculate. "Values" is the map: { "literal" : true/false }.
Verify the tautology
 By "verifying the tautology" I mean calculating the value for every combination of literals and making sure that it evaluates as "true" all the time. First thing is to extract all literals from the parsed string. It is received by a simple statement (assuming that 'e' is parsed expression)

distinct (filter #(and (not (nil? %)) (Character/isLetter  (first %))) (flatten e))

The number of all literal combination is 2 power {number of literals}. So generating all combinations can be achieved by iterating all integers from 0 to 2 power {number of literal} and extracting literal values from binary representation of the current integer (1 as true and 0 as false.

(defn genvalues [lvals num ]
     (defn getsinglevalue [k]
        [ (nth lvals k) (odd? (bit-shift-right num k)) ]
     )
     (map getsinglevalue (range 0 (count lvals)))
  )

The last but not least is the main "verify" function. The function returns a vector of values producing false. So the expression is tautology if the output list is empty.

(defn varifytautology

"verify if logical expression is tautology
 returns the collection of values giving false result
 if list is empty then expression is tautology
"

  [str]
  (let [ vals (calculateall str)]
;    (seq (for [x vals] (println x)))
    (reduce #( if (not (second %2 )) (conj %1 %2) %1) [] vals)
  )
)

Unit tests
The series of unit tests is provided with the source. Example

; DeMorgan's Low
(deftest parse-taut2
  (let [sent "(~(p & q) == (~p ^ ~q))"
        lfalse (logical.expression/varifytautology sent)
       ]
;   (println lfalse)   
    (is (empty? lfalse))
  )
)

; DeMorgan's Low
(deftest parse-taut3
  (let [sent "(~(p ^ q) == (~p & ~q))"
        lfalse (logical.expression/varifytautology sent)
       ]
;   (println lfalse)   
    (is (empty? lfalse))
  )
)

(deftest parse-taut4
  (let [sent "((a&b)=>c) == (a=>(b=>c))))"
        lfalse (logical.expression/varifytautology sent)
       ]
;   (println lfalse)   
    (is (empty? lfalse))
  )
)

; the Distribution Law
(deftest parse-taut5
  (let [sent "(p^(q&r)) == ((p^q)&(p^r))"
        lfalse (logical.expression/varifytautology sent)
       ]
;   (println lfalse)   
    (is (empty? lfalse))
  )
)

I'm happy to announce the De Morgan's Laws still holds true.