Partial Implementation of KE Method rules

ke.clj

(ns ke)


; formulas

(defrecord AtomicFormula [name])

(defrecord UnaryFormula [connective subformula])

(defrecord BinaryFormula [connective left-subformula right-subformula])

(defrecord SignedFormula [sign formula])


; patterns

(defn unary-signed-pattern 
  "Returns true if a signed formula is in a given pattern"
   [sign unary-connective signed-formula]
   (and (= sign (:sign signed-formula)) (= unary-connective (:connective (:formula signed-formula)))))
 

; builders

(defn unary-signed-remove-sign-remove-connective-include-sign-builder
  "Creates a new signed formula from another signed formula"
  [sign signed-formula]
  (->SignedFormula sign (:subformula (:formula signed-formula))))

; rules

;; unary linear rules

(defn t-not-rule 
   "Applies the T-NOT rule if the premise is a T-NOT signed-formula"
   [signed-formula-premise]
   (if (unary-signed-pattern :true :not signed-formula-premise) 
	(unary-signed-remove-sign-remove-connective-include-sign-builder :false signed-formula-premise)
	signed-formula-premise
  )
)

ke_tests.clj

(ns ke-tests
  (:use clojure.test)
  (:use ke))


; Atomic Formulas

(def anAtom (->AtomicFormula "A"))

(deftest test-atom-get-name
  (is (= "A"  (:name anAtom))))


; Unary Formulas

(def aUnaryFormula (->UnaryFormula :not anAtom))

(deftest test-unary-formula-get-connective
  (is (= :not  (:connective aUnaryFormula))))

(deftest test-unary-formula-get-subformula
  (is (= anAtom  (:subformula aUnaryFormula))))


; Binary Formulas

(def aBinaryFormula (->BinaryFormula :and anAtom aUnaryFormula))

(deftest test-binary-formula-get-connective
  (is (= :and  (:connective aBinaryFormula))))

(deftest test-binary-formula-get-left-subformula
  (is (= anAtom  (:left-subformula aBinaryFormula))))

(deftest test-binary-formula-get-right-subformula
  (is (= aUnaryFormula  (:right-subformula aBinaryFormula))))


; Signed Formulas

(def aSignedFormula (->SignedFormula :true aBinaryFormula))

(deftest test-signed-formula-get-sign
  (is (= :true (:sign aSignedFormula))))

(deftest test-signed-formula-get-formula
  (is (= aBinaryFormula (:formula aSignedFormula))))


; Some formula for next tests

(def atom-a (->AtomicFormula "A"))
(def f-a (->SignedFormula :false atom-a))
(def not-a (->UnaryFormula :not atom-a))
(def t-not-a (->SignedFormula :true not-a))


; Unary Signed Patterns

(deftest test-unary-signed-pattern 
  (is (unary-signed-pattern :true :not t-not-a)))


; Unary Signed Builders

(deftest test-unary-signed-remove-sign-remove-connective-include-sign
  (is (= f-a (unary-signed-remove-sign-remove-connective-include-sign-builder :false t-not-a))))

; Unary Linear Rules

;; T-NOT

(deftest test-t-not-rule
  (is (= f-a (t-not-rule t-not-a))))


;; TODO: represent tableaus -> the input is a partial tableau!

(run-tests)