diff --git a/gallery/example5.pdf b/gallery/example5.pdf
new file mode 100644
index 0000000..9adacb6
Binary files /dev/null and b/gallery/example5.pdf differ
diff --git a/gallery/example5.typ b/gallery/example5.typ
new file mode 100644
index 0000000..8a6bc2a
--- /dev/null
+++ b/gallery/example5.typ
@@ -0,0 +1,27 @@
+#import "/src/logic.typ": *
+#let F = $((not p -> q) or r) -> ((p and not r) or not q)$
+#let F = _implies(
+  _or(
+    _implies(
+      _not("p"),
+      "q"
+    ),
+    "r"
+  ),
+  _or(
+    _and(
+      "p",
+      _not("r")
+    ),
+    _not("q")
+  )
+)
+#display(F)
+#get-atoms(F)
+
+#get-components(F)
+
+#{
+  set text(size: 0.8em)
+  truth-table(F)
+}
\ No newline at end of file
diff --git a/src/logic.typ b/src/logic.typ
new file mode 100644
index 0000000..4ea4b82
--- /dev/null
+++ b/src/logic.typ
@@ -0,0 +1,165 @@
+#let _and(a, b) = (
+  type: "and",
+  a: a,
+  b: b
+)
+#let _or(a, b) = (
+  type: "or",
+  a: a,
+  b: b
+)
+#let _implies(a, b) = (
+  type: "implies",
+  a: a,
+  b: b
+)
+#let _not(a) = (
+  type: "not",
+  a: a
+)
+
+#let display(formula, first: true) = {
+  let display = display.with(first: false)
+  if type(formula) == str {
+    return formula
+  }
+  if type(formula) != dictionary {
+    panic("Invalid type")
+  }
+  let res = none
+  if formula.type == "and" {
+    res = $#display(formula.a) and #display(formula.b)$
+  } else if formula.type == "or" {
+    res = $#display(formula.a) or #display(formula.b)$
+  } else if formula.type == "implies" {
+    res = $#display(formula.a) -> #display(formula.b)$
+  } else if formula.type == "not" {
+    res = $not #display(formula.a)$
+  } else {
+    panic("Invalid type")
+  }
+  if not first and formula.type != "not" {
+    res = $(#res)$
+  }
+  return res
+}
+
+#let _walk(formula, callback) = {
+  let result = ()
+  if type(formula) == str {
+    result += callback(formula, result)
+  } else if type(formula) == dictionary {
+    result += callback(formula, result)
+    if formula.type in ("and", "or", "implies") {
+      result += _walk(formula.a, callback)
+      result += _walk(formula.b, callback)
+    } else if formula.type == "not" {
+      result += _walk(formula.a, callback)
+    }
+  }
+  return result
+}
+
+#let evaluate(formula, atoms-values) = {
+  if type(formula) == str {
+    return atoms-values.at(formula)
+  }
+  if type(formula) != dictionary {
+    panic("Invalid type")
+  }
+  if formula.type == "not" {
+    return 1 - evaluate(formula.a, atoms-values)
+  }
+  if not formula.type in ("and", "or", "implies") {
+    panic("Invalid type")
+  }
+  let a = evaluate(formula.a, atoms-values)
+  let b = evaluate(formula.b, atoms-values)
+  let cond = false
+  if formula.type == "and" {
+    cond = (a == 1 and b == 1)
+  } else if formula.type == "or" {
+    cond = (a == 1 or b == 1)
+  } else if formula.type == "implies" {
+    cond = (a == 0 or b == 1)
+  }
+  return if cond {1} else {0}
+}
+
+#let get-atoms(formula) = {
+  return _walk(formula, (a, res) => {
+    if type(a) == str {
+      res.push(a)
+    }
+    return res
+  }).dedup()
+}
+
+#let get-components(formula) = {
+  return _walk(formula, (a, res) => {
+    res.push(a)
+    return res
+  }).dedup()
+}
+
+#let get-level(formula) = {
+  if type(formula) == str {
+    return 0
+  }
+  if type(formula) != dictionary {
+    panic("Invalid type")
+  }
+  if formula.type in ("and", "or", "implies") {
+    return calc.max(
+      get-level(formula.a),
+      get-level(formula.b)
+    ) + 1
+  }
+  if formula.type == "not" {
+    return get-level(formula.a) + 1
+  }
+  panic("Invalid type")
+}
+
+#let truth-table(formula) = {
+  let atoms = get-atoms(formula).sorted()
+  let comps = get-components(formula)
+  let comps-lvls = comps.map(c => (c, get-level(c)))
+  let sorted = comps-lvls.sorted(key: cl => cl.last())
+
+  let cells = ()
+
+  let cur-lvl = 0
+  for (i, (comp, lvl)) in sorted.enumerate() {
+    if lvl != cur-lvl {
+      cells.push(table.vline())
+    } else if i != 0 {
+      cells.push(table.vline(stroke: (dash: "dashed")))
+    }
+    cur-lvl = lvl
+    cells.push(display(comp))
+  }
+  cells.push(table.hline())
+  for i in range(calc.pow(2, atoms.len())) {
+    if calc.rem(i, 4) == 0 and i != 0 {
+      cells.push(table.hline())
+    }
+    let atoms-values = (:)
+    for (j, a) in atoms.enumerate() {
+      let bit = i.bit-rshift(atoms.len() - j - 1).bit-and(1)
+      atoms-values.insert(a, bit)
+    }
+    for (comp, lvl) in sorted {
+      let value = evaluate(comp, atoms-values)
+      cells.push($#value$)
+    }
+  }
+
+  table(
+    columns: sorted.len(),
+    stroke: none,
+    align: center + horizon,
+    inset: (left: 0.5em, right: 0.5em, top: 0.4em, bottom: 0.4em),
+    ..cells
+  )
+}
\ No newline at end of file