using katex instead

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"]

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.

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
 

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