From 0a72f4915c8736c82f64ccd37d891db90890af2a Mon Sep 17 00:00:00 2001
From: Andrew Chen <andrewchen14250@gmail.com>
Date: Thu, 9 Jan 2025 23:50:55 -0500
Subject: [PATCH] using katex instead

---
 book.toml                                     |  5 ++-
 .../cryptol_for_haskell_knowers/front.md      |  2 +-
 src/glossary_resources.md                     |  2 +-
 src/smt_solvers/front.md                      | 37 +++++++++++++++++++
 4 files changed, 42 insertions(+), 4 deletions(-)

diff --git a/book.toml b/book.toml
index ea59c92..5331859 100644
--- a/book.toml
+++ b/book.toml
@@ -5,5 +5,6 @@ multilingual = false
 src = "src"
 title = "A Journey Through Formal Methods"
 
-[output.html]
-mathjax-support = true
+
+[preprocessor.katex]
+after = ["links"]
\ No newline at end of file
diff --git a/src/full_applications/verified_cryptography/cryptol_for_haskell_knowers/front.md b/src/full_applications/verified_cryptography/cryptol_for_haskell_knowers/front.md
index b2fbd2d..60f5a1e 100644
--- a/src/full_applications/verified_cryptography/cryptol_for_haskell_knowers/front.md
+++ b/src/full_applications/verified_cryptography/cryptol_for_haskell_knowers/front.md
@@ -125,7 +125,7 @@ to be a proper sum of some sort is if additions wrap around (overflow).
 As a side note, `Ring` and `Field` are algebraic structures. The set of integers form a `Ring` because 
 we can define `(+)` and `(*)` according to a set of rules. However, the set of integers do not form 
 a `Field`, which requires every nonzero element to have a multiplicative inverse. The prototypical
-example of a `Field` is the set of integers modulo \\( m \\) with \\( m \\) prime.
+example of a `Field` is the set of integers modulo $ m $ with $ m $ prime.
 
 The last piece worth mentioning is arithmetic type inferencing. I illustrate these with examples instead of describing
 rules.
diff --git a/src/glossary_resources.md b/src/glossary_resources.md
index 291d637..6f1fba6 100644
--- a/src/glossary_resources.md
+++ b/src/glossary_resources.md
@@ -1,5 +1,5 @@
 # Glossary and Resources
 
 ## Resources
-[Model Checking](https://mitpress.ublish.com/ebook/model-checking-2e-preview/7092/ix): Temporal Logics, Automata, SAT, \\( \mu \\)-Calculus, concurrency
+[Model Checking](https://mitpress.ublish.com/ebook/model-checking-2e-preview/7092/ix): Temporal Logics, Automata, SAT, $ \mu $-Calculus, concurrency
 
diff --git a/src/smt_solvers/front.md b/src/smt_solvers/front.md
index 06e9e1d..febb395 100644
--- a/src/smt_solvers/front.md
+++ b/src/smt_solvers/front.md
@@ -1 +1,38 @@
 # SMT_Solvers
+
+
+Unfiltered notes below:
+
+## 1. A History of Satisfiability
+The history of satisfiability is best understood along its logic roots.
+
+In logic, syntax and semantics are distinct.
+
+Syntax is associated with proof theory, syntactic derivation, axioms
+with a specified grammatical forms, inference rules. 
+
+Semantics deals with model theory, satisfiability with respect to worlds.
+
+In logic, there are two key terms: validity and consistency. They are interdefinable.
+if we make use of $\neg$:
+the argument from $ p_1,\dots,p_n $ to $ q $ is valid if and only if the
+set $ \set{p_1, \dots, p_n, \neg q} $ is inconsistent. 
+
+In proof theory, validity is called derivability. Consistency is just called consistency. 
+
+Derivability: $ q $ is derivable 
+from $ p_1, \dots, p_n $ (in symbols, $ p_1, \dots, p_n \vdash q $)
+if and only if you can syntactically prove you using inference rules.there is a proof in the axiom system.
+
+In model theory, validity is just called validity. Consistency is called satisfiability. $ A \vDash p $ means that $ p $
+is true in the structure $ A $. 
+
+Satisfiability, or semantic consistency: $ \set{p_1, \dots, p_n} $ is satisfiable
+if and only if for some $ A, A \vDash p_1, \dots, A \vDash p_n $.
+
+
+An axiom system is 
+
+
+## Resources
+Handbook of satisfiability
\ No newline at end of file