Merge pull request #45 from ryukinix/fixing-old-issues

feat: resolve 5+ years old issues

Author: ryukinix

run-test.lisp

@@ -1,5 +1,11 @@
 (load "fix-quicklisp")
 (ql:quickload :lisp-inference/tests :silent t)
+
+(defun rove/utils/reporter::print-source-location-as-file-path (stream file line column)
+  (declare (ignore column))
+  (format stream "~&at ~A~@[:~A~]~%"
+          (rove/utils/reporter::enough-namestring* file)
+          line))
 (setf rove:*enable-colors* t)
 (if (rove:run :lisp-inference/tests)
     (sb-ext:exit :code 0)

src/equivalences.lisp

@@ -49,3 +49,11 @@
           (make-negation (make-conjunction (make-negation (first-operand exp))
                                            (make-negation (second-operand exp)))))
          (t exp))))
+
+(defun implication (exp)
+  "Implication equivalence ::
+  (=> p q) <=> (v (~ p) q)"
+  (if (implicationp exp)
+      (make-disjunction (make-negation (first-operand exp))
+                        (second-operand exp))
+      exp))

src/inferences.lisp

@@ -42,8 +42,8 @@
                       (operands (first-operand exp))))
       exp))
 
-(defun addiction (exp p)
-  "Addiction in inference rule ::
+(defun addition (exp p)
+  "Addition in inference rule ::
    p => (v p q)"
   (make-disjunction exp p))
 

src/package.lisp

@@ -7,10 +7,11 @@
   (:use #:cl #:cl-user)
   (:export #:double-negation ;; equivalences
            #:de-morgan
+           #:implication
            #:modus-ponens    ;; inferences
            #:modus-tollens
            #:syllogism-disjunctive
-           #:addiction
+           #:addition
            #:conjunction
            #:simplification-first
            #:simplification-second
@@ -33,7 +34,9 @@
            #:^
            #:v
            #:=>
+           #:->
            #:<=>
+           #:<->
            #:[+]
            #:make-conjunction
            #:make-negation

src/parser.lisp

@@ -76,12 +76,14 @@
 (defun implicationp (exp)
   "Verify if the expression is an implication"
   (and (binary-operationp exp)
-       (operationp exp '=>)))
+       (or (operationp exp '=>)
+           (operationp exp '->))))
 
 (defun biconditionalp (exp)
   "Verify if the expression is a biconditional"
   (and (binary-operationp exp)
-       (operationp exp '<=>)))
+       (or (operationp exp '<=>)
+           (operationp exp '<->))))
 
 (defun swap-operand-operator (exp)
   (if (and (listp exp)

src/truth-table.lisp

@@ -75,7 +75,7 @@
 ;; the function is O(2^n) time, so I think is not a good idea put inside of it.
 
 ;; RECURSIVE BOMB, BE CAREFUL
-(defun stack-of-expressions (exp)
+(defun %stack-of-expressions (exp)
   "Based on propositional EXP generate a stack of expressions
    to be evaluated on truth-table generation"
   (cond ((and (valid-operationp exp)
@@ -93,6 +93,8 @@
            expressions))
         (t nil)))
 
+(defun stack-of-expressions (exp)
+  (remove-duplicates (%stack-of-expressions exp) :test #'equal))
 
 (defun replace-tf (exp)
   (cond ((atom exp)

t/test-equivalence-rules.lisp

@@ -1,22 +1,31 @@
 (in-package #:lisp-inference/tests/test-equivalence-rules)
 
 (deftest test-equivalence-rules
-  (testing "== Equivalence rules!"
-    (ok (equal (de-morgan '(^ p q))
-               '(~ (v (~ p) (~ q))))
-        "Equivalence: DE-MORGAN 1")
-    (ok (equal (de-morgan '(~ (v p q)))
-               '(^ (~ p) (~ q)))
-        "Equivalence: DE-MORGAN 2")
+    (testing "== Equivalence rules!"
+             (ok (equal (de-morgan '(^ p q))
+                        '(~ (v (~ p) (~ q))))
+                 "Equivalence: DE-MORGAN 1")
+             (ok (equal (de-morgan '(~ (v p q)))
+                        '(^ (~ p) (~ q)))
+                 "Equivalence: DE-MORGAN 2")
 
-    (ok (equal (de-morgan '(~ (^ (~ p) (~ q))))
-               '(v p q))
-        "Equivalence: DE-MORGAN 3")
+             (ok (equal (de-morgan '(~ (^ (~ p) (~ q))))
+                        '(v p q))
+                 "Equivalence: DE-MORGAN 3")
 
-    (ok (equal (double-negation '(~ (~ p)))
-               'p)
-        "Equivalence: DOUBLE-NEGATION 1")
+             (ok (equal (double-negation '(~ (~ p)))
+                        'p)
+                 "Equivalence: DOUBLE-NEGATION 1")
 
-    (ok (equal (double-negation 'p)
-               'p)
-        "Equivalence: DOUBLE-NEGATION 2")))
+             (ok (equal (double-negation 'p)
+                        'p)
+                 "Equivalence: DOUBLE-NEGATION 2")
+             (ok (equal (implication '(=> p q))
+                        '(v (~ p) q))
+                 "Equivalence: IMPLICATION EQUIVALENCE")
+
+             (ok (equal (implication '(-> p (~ q)))
+                        '(v (~ p) (~ q)))
+                 "Equivalence: IMPLICATION EQUIVALENCE 2")
+
+             ))

t/test-inference-rules.lisp

@@ -19,9 +19,9 @@
                '(=> X Z))
         "Inference: SYLLOGISM-HYPOTHETICAL")
 
-    (ok (equal (addiction 'p 'q)
+    (ok (equal (addition 'p 'q)
                '(v p q))
-        "Inference: ADDICTION")
+        "Inference: ADDITION")
 
     (ok (equal (conjunction '(=> p q) 'p)
                '(^ (=> P Q) P))

t/test-truth-table.lisp

@@ -53,3 +53,8 @@
                    (print-truth-table '(^ (=> p q) r)))
                'simple-error)
         "Raise a error when there is more propositions than specified at *MAX-PROPOSITIONS*"))
+
+
+(deftest truth-table-without-duplicated-stack-of-expressions
+  (ok (equal (inference::stack-of-expressions '(^ (~ p) (~ p)))
+             '((~ p) (^ (~ p) (~ p))))))