diff --git a/docs/tutorial/tutorial.md b/docs/tutorial/tutorial.md
index f44b54c8..c841178b 100644
--- a/docs/tutorial/tutorial.md
+++ b/docs/tutorial/tutorial.md
@@ -116,7 +116,7 @@ Let's start with the simplest rule, Wf-Kind:
 wf(G, T, k_star) :- wf(G, T, k_base).
 ```
 
-Horn clauses are read right to left, so this rule is saying that types that are well-formed at kind base are also well-formed at kind star.
+Horn clauses are implications (read right to left), so this rule is saying that types that are well-formed at kind base are also well-formed at kind star.
 Identifiers beginning with an uppercase letter are logic programming variables, which are implicitly universally quantified across the entire rule.
 
 Wf-Fun is not too bad to encode either:
@@ -154,7 +154,7 @@ We can then encode the rule for boolean literals:
 pred_wf(_G, p_bool(_B), b_bool).
 ```
 
-The rules for most the other constructs is straightforward:
+The rules are straightforward for most of the other constructs:
 
 ```
 pred_wf(_G, p_int(_I), b_int).
@@ -182,7 +182,7 @@ pred_wf(G, p_ite(P1, P2, P3), T) :-
     pred_wf(G, P3, T).
 ```
 
-The leaves us just handling variables; to do so, we need to define what it means to look up a variable in an environment.
+That leaves us just handling variables; to do so, we need to define what it means to look up a variable in an environment.
 Formulog's first-order functional programming comes in handy for defining this type of helper function:
 
 ```
@@ -772,4 +772,4 @@ As we mentioned earlier, please raise a [GitHub issue](https://github.com/Harvar
 
 [3] Yu Feng, Xinyu Wang, Isil Dillig, and Thomas Dillig. 2015. Bottom-up Context-Sensitive Pointer Analysis for Java. In Proceedings of the 13th Asian Symposium on Programming Languages and Systems. 465–484. https://doi.org/10.1007/978-3-319-26529-2_25
 
-[4] Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. 209–224. https://www.usenix.org/legacy/event/osdi08/tech/full_papers/cadar/cadar.pdf
\ No newline at end of file
+[4] Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. 209–224. https://www.usenix.org/legacy/event/osdi08/tech/full_papers/cadar/cadar.pdf