diff --git a/README.md b/README.md
index 66fa841..c5eae79 100644
--- a/README.md
+++ b/README.md
@@ -1,18 +1,18 @@
 Not really usable as a fully fledged SMT solver right now.
-Mainly just a collection of the various algorithms used in SMT solvers, implemented in Haskell:
+Mainly just a collection of various algorithms used in SMT solvers, implemented in Haskell:
 
 * SAT solving
-  * [x] [Davis–Putnam–Logemann–Loveland (DPLL)](/src/SAT/DPLL.hs)
-  * [x] [Conflict Driven Clause Learning (CDCL)](/src/SAT/CDCL.hs)
+  * [Davis–Putnam–Logemann–Loveland (DPLL)](/src/SAT/DPLL.hs)
+  * [Conflict Driven Clause Learning (CDCL)](/src/SAT/CDCL.hs)
 * Uninterpreted Functions
-  * [x] [Congruence Closure](/src/Theory/UninterpretedFunctions.hs)
+  * [Congruence Closure](/src/Theory/UninterpretedFunctions.hs)
 * Linear Arithmatic
-  * [x] [Simplex Method](/src/Theory/LinearArithmatic/Simplex.hs)
-  * [x] [Fourier-Motzkin](/src/Theory/LinearArithmatic/FourierMotzkin.hs)
-  * [x] [Branch and Bound](/src/Theory/LinearArithmatic/FourierMotzkin.hs)
+  * [Simplex Method](/src/Theory/LinearArithmatic/Simplex.hs)
+  * [Fourier-Motzkin](/src/Theory/LinearArithmatic/FourierMotzkin.hs)
+  * [Branch and Bound](/src/Theory/LinearArithmatic/BranchAndBound.hs)
 * Non-Linear Arithmatic
-  * [ ] [Interval Constraint Propagation](/src/Theory/NonLinearArithmatic/IntervalConstraintPropagation.hs)
-  * [ ] [Subtropical Satisfiability](/src/Theory/NonLinearArithmatic/Subtropical.hs)
-  * [ ] [Cylindtrical Algebraic Decomposition](/src/Theory/NonLinearArithmatic/CAD.hs)
-  * [ ] Virtual Substitution
+  * [Interval Constraint Propagation](/src/Theory/NonLinearRealArithmatic/IntervalConstraintPropagation.hs)
+  * [Subtropical Satisfiability](/src/Theory/NonLinearRealArithmatic/Subtropical.hs)
+  * [Cylindtrical Algebraic Decomposition](/src/Theory/NonLinearRealArithmatic/CAD.hs)
+  * Virtual Substitution