diff --git a/src/nal.rs b/src/nal.rs
index c4fb4fc..8f605da 100644
--- a/src/nal.rs
+++ b/src/nal.rs
@@ -1,11 +1,11 @@
 //! Non-Axiomatic Logic fuctionality
 pub mod formulas;
 pub mod parser;
+pub mod rules;
 
-use nom::sequence::Tuple;
 use serde::{Deserialize, Serialize};
 
-#[derive(Serialize, Deserialize)]
+#[derive(Clone, Copy, Serialize, Deserialize)]
 struct EvidentialValue {
     s: f32,
     c: f32,
@@ -41,7 +41,7 @@ impl EvidentialValue {
 /// # Panics
 /// The strength / frequency must lie in the interval [0.0; 1.0].
 /// The confidence must lie in the interval [0.0; 1.0).
-#[derive(Serialize, Deserialize)]
+#[derive(Clone, Copy, Serialize, Deserialize)]
 pub struct TruthValue {
     ev: EvidentialValue,
 }
@@ -52,13 +52,13 @@ impl TruthValue {
             ev: EvidentialValue::new(strength, confidence),
         }
     }
-
     pub fn strength(&self) -> f32 {
         self.ev.s
     }
     pub fn confidence(&self) -> f32 {
         self.ev.c
     }
+
     fn from(maybe_tvstr: Option<(&str, &str)>) -> Option<TruthValue> {
         maybe_tvstr.and_then(|(s, c)| {
             let strength = s.parse::<f32>().ok()?;
@@ -75,7 +75,7 @@ impl TruthValue {
 /// # Panics
 /// The strength / frequency must lie in the interval [0.0; 1.0].
 /// The confidence must lie in the interval [0.0; 1.0).
-#[derive(Serialize, Deserialize)]
+#[derive(Clone, Copy, Serialize, Deserialize)]
 pub struct DesireValue {
     ev: EvidentialValue,
 }
@@ -125,21 +125,21 @@ impl Tense {
 
 #[derive(Serialize, Deserialize)]
 pub struct Judgement {
-    pub term: AtomicTerm,
+    pub term: Term,
     pub tv: TruthValue,
     pub tense: Tense,
 }
 
 #[derive(Serialize, Deserialize)]
 pub struct Question {
-    pub term: AtomicTerm,
+    pub term: Term,
     pub tv: TruthValue,
     pub tense: Tense,
 }
 
 #[derive(Serialize, Deserialize)]
 pub struct Goal {
-    pub term: AtomicTerm,
+    pub term: Term,
     pub d: DesireValue,
     pub tense: Tense,
 }
@@ -155,10 +155,19 @@ impl Sentence {
     pub fn from(sttv: ((&str, &str), Tense, Option<(&str, &str)>)) -> Result<Self, String> {
         let ((expr, pstr), tense, tvstr) = sttv;
 
-        let term = Term::Atom(TermInfo {
-            id: 0,
-            expr: String::from(expr),
-        });
+        // let term = Term::Atom(TermInfo {
+        //     id: 0,
+        //     expr: String::from(expr),
+        // });
+        let term = Term {
+            info: TermInfo {
+                id: 0,
+                expr: String::from(expr),
+                tv: TruthValue {
+                    ev: EvidentialValue { s: 1.0, c: 0.9 },
+                },
+            },
+        };
         let punctuation = pstr.chars().last();
         let tv = TruthValue::from(tvstr).unwrap_or(TruthValue::new(1.0, 0.5));
         match punctuation {
@@ -177,25 +186,22 @@ impl Sentence {
 // terms
 
 #[derive(Serialize, Deserialize)]
-struct TermInfo {
+pub struct TermInfo {
     pub id: u32,
     pub expr: String,
+    pub tv: TruthValue,
 }
 
-#[derive(Serialize, Deserialize)]
-pub enum Term {
-    Atom(TermInfo),
-    Compound(TermInfo),
-}
-// pub struct AtomicTerm {
-// info: TermInfo,
+// #[derive(Serialize, Deserialize)]
+// pub enum Term {
+//     Atom(TermInfo),
+//     Compound(TermInfo),
 // }
 
-// impl Term {
-//     pub fn new(expr: &str) -> Self { Self { info: TermInfo { id: 0, expr: String::from(expr) } } }
-
-//     pub fn name(&self) -> &str { &self.info.expr }
-// }
+#[derive(Serialize, Deserialize)]
+pub struct Term {
+    pub info: TermInfo,
+}
 
 enum VarT {
     Independent,
diff --git a/src/nal/formulas.rs b/src/nal/formulas.rs
index 4203fd3..cb81217 100644
--- a/src/nal/formulas.rs
+++ b/src/nal/formulas.rs
@@ -3,113 +3,124 @@
 use super::TruthValue;
 
 // (= (Truth_w2c $w) (/ $w (+ $w 1)))
-fn truth_w2c(w: f32) -> f32 {
+pub fn truth_w2c(w: f32) -> f32 {
     w / (w + 1.0)
 }
 
-// (= (Truth_Deduction ($f1 $c1) ($f2 $c2)) ((* $f1 $f2) (* (* $f1 $f2) (* $c1 $c2))))
-fn truth_deduction(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    TruthValue::new(f1 * f2, f1 * f2 * c1 * c2)
+pub fn deduction(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    TruthValue::new(
+        tv1.strength() * tv2.strength(),
+        tv1.strength() * tv2.strength() * tv1.confidence() * tv2.confidence(),
+    )
 }
 
-// (= (Truth_Abduction ($f1 $c1) ($f2 $c2)) ($f2 (Truth_w2c (* (* $f1 $c1) $c2))))
-fn truth_abduction(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    TruthValue::new(f2, truth_w2c(f1 * c1 * c2))
+pub fn abduction(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    TruthValue::new(
+        tv2.strength(),
+        truth_w2c(tv1.strength() * tv1.confidence() * tv2.confidence()),
+    )
 }
 
-// (= (Truth_Induction $T1 $T2) (Truth_Abduction $T2 $T1))
-fn truth_induction(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    truth_abduction(f2, c2, f1, c1)
+pub fn induction(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    abduction(tv2, tv1)
 }
 
-// (= (Truth_Exemplification ($f1 $c1) ($f2 $c2)) (1.0 (Truth_w2c (* (* $f1 $f2) (* $c1 $c2)))))
-fn truth_exemplification(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    TruthValue::new(1.0, truth_w2c(f1 * f2 * c1 * c2))
+pub fn exemplification(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    TruthValue::new(
+        1.0,
+        truth_w2c(tv1.strength() * tv2.strength() * tv1.confidence() * tv2.confidence()),
+    )
 }
 
-// (= (Truth_StructuralDeduction $T) (Truth_Deduction $T (1.0 0.9)))
-fn truth_structural_deduction(f1: f32, c1: f32) -> TruthValue {
-    truth_deduction(f1, c1, 1.0, 0.9)
+pub fn structural_deduction(tv1: TruthValue) -> TruthValue {
+    let tv = TruthValue::new(1.0, 0.9);
+    deduction(tv1, tv)
 }
 
-// (= (Truth_Negation ($f $c)) ((- 1 $f) $c))
-fn truth_negation(f: f32, c: f32) -> TruthValue {
-    TruthValue::new(1.0 - f, c)
+pub fn negation(tv1: TruthValue) -> TruthValue {
+    TruthValue::new(1.0 - tv1.strength(), tv1.confidence())
 }
 
-// (= (Truth StructuralDeductionNegated $T) (Truth_Negation (Truth_StructuralDeduction $T)))
-fn truth_structural_deduction_negated(f1: f32, c1: f32) -> TruthValue {
-    let tsd = truth_structural_deduction(f1, c1);
-    truth_negation(tsd.0, tsd.1)
+pub fn structural_deduction_negated(tv1: TruthValue) -> TruthValue {
+    let tsd = structural_deduction(tv1);
+    negation(tsd)
 }
-// (= (Truth_Intersection ($f1 $c1) ($f2 $c2)) ((* $f1 $f2) (* $c1 $c2)))
-fn truth_intersection(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    TruthValue::new(f1 * f2, c1 * c2)
+
+pub fn intersection(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    TruthValue::new(
+        tv1.strength() * tv2.strength(),
+        tv1.confidence() * tv2.confidence(),
+    )
 }
 
-// (= (Truth_StructuralIntersection $T) (Truth_Intersection $T (1.0 0.9)))
-fn truth_structural_intersection(f1: f32, c1: f32) -> TruthValue {
-    truth_intersection(f1, c1, 1.0, 0.9)
+pub fn structural_intersection(tv1: TruthValue) -> TruthValue {
+    let tv = TruthValue::new(1.0, 0.9);
+    intersection(tv1, tv)
 }
 
-// (= (Truth_or $a $b) (- 1 (* (- 1 $a) (- 1 $b))))
-fn truth_or(a: f32, b: f32) -> f32 {
+pub fn or(a: f32, b: f32) -> f32 {
     1.0 - (1.0 - a) * (1.0 - b)
 }
 
-// (= (Truth_Comparison ($f1 $c1) ($f2 $c2)) (let $f0 (Truth_or $f1 $f2) ((if (== $f0 0.0) 0.0 (/ (* $f1 $f2) $f0)) (Truth_w2c (* $f0 (* $c1 $c2))))))
-fn truth_comparison(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    let f0 = truth_or(f1, f2);
-    let f_ans: f32 = if f0 == 0.0 { 0.0 } else { (f1 * f2) / f0 };
-    TruthValue::new(f_ans, truth_w2c(f0 * c1 * c2))
+pub fn comparison(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    let f0 = or(tv1.strength(), tv2.strength());
+    let f_ans = if f0 == 0.0 {
+        0.0
+    } else {
+        (tv1.strength() * tv2.strength()) / f0
+    };
+    TruthValue::new(f_ans, truth_w2c(f0 * tv1.confidence() * tv2.confidence()))
 }
 
-// (= (Truth_Analogy ($f1 $c1) ($f2 $c2)) ((* $f1 $f2) (* (* $c1 $c2) $f2)))
-fn truth_analogy(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    TruthValue::new(f1 * f2, c1 * c2 * f2)
+pub fn analogy(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    TruthValue::new(
+        tv1.strength() * tv2.strength(),
+        tv1.confidence() * tv2.confidence() * tv2.strength(),
+    )
 }
 
-// (= (Truth_Resemblance ($f1 $c1) ($f2 $c2)) ((* $f1 $f2) (* (* $c1 $c2) (Truth_or $f1 $f2))))
-fn truth_resemblance(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    TruthValue::new(f1 * f2, c1 * c2 * truth_or(f1, f2))
+pub fn resemblance(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    TruthValue::new(
+        tv1.strength() * tv2.strength(),
+        tv1.confidence() * tv2.confidence() * or(tv1.strength(), tv2.strength()),
+    )
 }
 
-// (= (Truth_Union ($f1 $c1) ($f2 $c2)) ((Truth_or $f1 $f2) (* $c1 $c2)))
-fn truth_union(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    TruthValue::new(truth_or(f1, f2), c1 * c2)
+pub fn union(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    TruthValue::new(
+        or(tv1.strength(), tv2.strength()),
+        tv1.confidence() * tv2.confidence(),
+    )
 }
 
-// (= (Truth_Difference ($f1 $c1) ($f2 $c2)) ((* $f1 (- 1 $f2)) (* $c1 $c2)))
-fn truth_difference(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    TruthValue::new(f1 * (1.0 - f2), c1 * c2)
+pub fn difference(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    TruthValue::new(
+        tv1.strength() * (1.0 - tv2.strength()),
+        tv1.confidence() * tv2.confidence(),
+    )
 }
 
-// (= (Truth_DecomposePNN ($f1 $c1) ($f2 $c2)) (let $fn (* $f1 (- 1 $f2)) ((- 1 $fn) (* $fn (* $c1 $c2)))))
-fn truth_decompose_pnn(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    let fn_ = f1 * (1.0 - f2);
-    TruthValue::new(1.0 - fn_, fn_ * c1 * c2)
+pub fn decompose_pnn(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    let fn_ = tv1.strength() * (1.0 - tv2.strength());
+    TruthValue::new(1.0 - fn_, fn_ * tv1.confidence() * tv2.confidence())
 }
 
-// (= (Truth_DecomposeNPP ($f1 $c1) ($f2 $c2)) (let $f (* (- 1 $f1) $f2) ($f (* $f (* $c1 $c2)))))
-fn truth_decompose_npp(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    let f = (1.0 - f1) * f2;
-    TruthValue::new(f, f * c1 * c2)
+pub fn decompose_npp(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    let f = (1.0 - tv1.strength()) * tv2.strength();
+    TruthValue::new(f, f * tv1.confidence() * tv2.confidence())
 }
 
-// (= (Truth_DecomposePNP ($f1 $c1) ($f2 $c2)) (let $f (* $f1 (- 1 $f2)) ($f (* $f (* $c1 $c2)))))
-fn truth_decompose_pnp(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    let f = f1 * (1.0 - f2);
-    TruthValue::new(f, f * c1 * c2)
+pub fn decompose_pnp(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    let f = tv1.strength() * (1.0 - tv2.strength());
+    TruthValue::new(f, f * tv1.confidence() * tv2.confidence())
 }
 
-// (= (Truth_DecomposePPP $v1 $v2) (Truth_DecomposeNPP (Truth_Negation $v1) $v2))
-fn truth_decompose_ppp(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    let negtv = truth_negation(f1, c1);
-    truth_decompose_npp(negtv.strength(), negtv.confidence(), f2, c2)
+pub fn decompose_ppp(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    let negtv = negation(tv1);
+    decompose_npp(negtv, tv2)
 }
 
-// (= (Truth_DecomposeNNN ($f1 $c1) ($f2 $c2)) (let $fn (* (- 1 $f1) (- 1 $f2)) ((- 1 $fn) (* $fn (* $c1 $c2)))))
-fn truth_decompose_nnn(f1: f32, c1: f32, f2: f32, c2: f32) -> TruthValue {
-    let fn_ = (1.0 - f1) * (1.0 - f2);
-    TruthValue::new(1.0 - fn_, fn_ * c1 * c2)
+pub fn decompose_nnn(tv1: TruthValue, tv2: TruthValue) -> TruthValue {
+    let fn_ = (1.0 - tv1.strength()) * (1.0 - tv2.strength());
+    TruthValue::new(1.0 - fn_, fn_ * tv1.confidence() * tv2.confidence())
 }
diff --git a/src/nal/rules.rs b/src/nal/rules.rs
index 1ad8439..a023169 100644
--- a/src/nal/rules.rs
+++ b/src/nal/rules.rs
@@ -2,7 +2,21 @@
 // NAL-1
 // Syllogistic rules for Inheritance
 
+use super::formulas::*;
+use super::Term;
+use super::TermInfo;
+use super::TruthValue;
+
 // (= (|- (($a --> $b) $T1) (($b --> $c) $T2)) (($a --> $c) (Truth_Deduction $T1 $T2)))
-fn term_rewrite_deduction(fa: f32, ca: f32, fb: f32, cb: f32, fc: f32, cc: f32) -> (f32, f32) {
-    truth_deduction(fa, ca, fb, cb, fc, cc)
+pub fn rewrite_deduction(tab: Term, tbc: Term) -> (Term, TruthValue) {
+    let expr_deduction: String = format!("<{} --> {}>", tab.info.expr, tbc.info.expr);
+    let tv_deduction: TruthValue = deduction(tab.info.tv, tbc.info.tv);
+    let term_deduction: Term = Term {
+        info: TermInfo {
+            id: 0,
+            expr: expr_deduction,
+            tv: tv_deduction,
+        },
+    };
+    (term_deduction, tv_deduction)
 }