diff --git a/logic/README.md b/logic/README.md
index 31a9454..03e0360 100644
--- a/logic/README.md
+++ b/logic/README.md
@@ -1 +1,12 @@
 satisfy them booleans, solve them integers.
+
+`cnf.py` is a small library for creating formulas in conjunctive normal form,
+and also for dealing with the eponymous CNF file format.
+the types used internally and exposed externally are very simple:
+booleans, integers, and lists of each.
+
+`z0.py` is a slightly larger library that builds upon `cnf.py`,
+mimicing a tiny subset of the [z3](https://github.com/Z3Prover/z3)
+library's interface. it exposes classes for high-level bitvectors and
+[unary-encoded integers.](https://en.wikipedia.org/wiki/Unary_numeral_system)
+(unary is sometimes more efficient to solve)