diff --git a/README.md b/README.md
index dbd80db..1815d7f 100644
--- a/README.md
+++ b/README.md
@@ -1,35 +1,143 @@
-# Дедуктивный решатель
+# Deductive Solver
 
-Определением *x* можно называть такое правило, которое делит все существующие (а также мыслимые) индвидуальные предметы в нашем мире на две части: соответствующие определению *x* и не соответствующие *¬x*.
+A *definition* of *x* may be called a rule that divides every existing (and every conceivable) individual object in our world into two parts: those that match the definition *x*, and those that do not, *¬x*.
 
-Тем не менее, если предметные науки формируют понятийный аппарат, то логика изучает соотношения понятий между собой. Понятия существуют на множестве всех рассматриваемых предметов.
+While the subject sciences build up a conceptual apparatus, logic studies how concepts relate to one another. Concepts live over the set of all objects under consideration.
 
-Как справедливо отмечает польская математическая традиция с одной стороны и Н.П.Брусенцов с другой стороны, символ "существования" некоторого предмета, записываемый как ∀, на самом деле имеет тесную связь с дизъюнкцией: ∨. Конкретно, это "интегральная" дизъюнкция, дизъюнкция по множеству: Vx значит, что мы пытаемся перебрать все предметы на предмет соответствия x, и если хотя бы один из них подходит, то дизъюнкция по множеству так же существует на всём множестве.
+As the Polish mathematical tradition on the one hand and N. P. Brusentsov on the other rightly point out, the symbol of "existence" of some object, written as ∃, is in fact closely related to disjunction, ∨. Specifically, it is an "integral" disjunction — a disjunction over a set: V*x* means that we run through every object checking it against *x*, and if at least one of them fits, then the set-wide disjunction holds over the whole set as well.
 
-Расширяя множества до нечётких (в которых элементы могут достоверно присутствовать, достоверно отсутствовать и быть свободными), мы можем рассматривать логические понятия во всех их соотношениях.
+By extending sets to three-valued ones — in which an element may be definitely present, definitely absent, or free — we can examine logical concepts in all of their relations.
 
-Современная математическая логика, как правило, работает совмещением признаков (или анти-признаки, то есть несоответстветствия признакам) предметов булевской алгеброй, без нечётких множеств. Такой подход позволяет достичь больших успехов в описании отдельно взятого предмета в заранее определённой системе понятий. В то же время, такой подход плохо подходит для описания **систем**, точнее, он требует описывать системы как единые предметы, что чаще всего крайне неестественно.
+Modern mathematical logic normally combines the features of objects (or anti-features, i.e. failures to match a feature) using Boolean algebra, without three-valued sets. That approach is very successful at describing a single object within a conceptual system fixed in advance. At the same time, it is a poor fit for describing **systems**: more precisely, it forces systems to be described as single objects, which is usually deeply unnatural.
 
-Решением же проблемы является рассмотрение алгебры нечётких множеств относительно комбинаций понятий. К примеру, Vxy означает, что среди всего множества предметов существует предмет, совместивший в себе признаки x и y, а V'xy' напротив, обозначает, что не бывает x без y (что, при дополнительных допущениях, является отношением следования).
+The solution is to consider the algebra of three-valued sets over *combinations* of concepts. For example, V*xy* means that somewhere in the set of objects there exists an object combining the features *x* and *y*, whereas V'*xy*' means the opposite: there is no *x* without *y* (which, under additional assumptions, is the relation of entailment).
 
-Данная концепция упоминается в книгах коллектива авторов, создавших компьютер "Сетунь" - прежде всего, книгах Н.П. Брусенцова. Наиболее полно эта концепция раскрыта в его книгах "Начала информатики" и "Искусство достоверного рассуждения".
+This idea is discussed in the books of the team that built the "Setun" computer — above all in the books of N. P. Brusentsov. It is presented most fully in his *Foundations of Informatics* (Начала информатики) and *The Art of Reliable Reasoning* (Искусство достоверного рассуждения).
 
-Дедуктивный решатель работает с составными логическими понятиями (например xy'z - это событие или предмет, совместивший в себе x, не-y и z), а также фактами (дизъюнкциями по множеству понятий или отрицаниями этих дизъюнкций).
+The deductive solver works with compound logical concepts (for example *xy'z* — an event or object combining *x*, not-*y*, and *z*) and with facts (set-wide disjunctions over such concepts, or negations of those disjunctions).
 
-## 4 правила (диаграмма Льюиса Кэррола)
+## The four rules (Lewis Carroll's diagram)
 
-Чарльз Доджсон, также известный как Льюис Кэррол, активно исследовал вопросы логики. Он создал диаграмму табличного вида (отчасти напоминающую клеточный автомат или игру), которая позволяет осуществлять логические вычисления. Обобщая, можно сформулировать 4 применяемых к понятиям правила, два из которых "очевидны", а два создают "новую" информацию:
+Charles Dodgson, better known as Lewis Carroll, studied questions of logic intensively. He devised a tabular diagram — somewhat reminiscent of a cellular automaton or a game — that allows logical computation to be carried out. Generalizing it, one can state four rules applied to concepts, two of which are "obvious" and two of which create "new" information:
 
-1. **Восходящая истина (очевидный).** "Если существует вид xyz' (Vxyz'), то существуют все его рода Vx, Vy, Vz', Vxy, Vxz', Vyz', кроме того существует неопределенное нечто V (абсолютно неспецифичное понятие)" 
+1. **Upward truth (obvious).** "If the species V*xyz*' exists, then all of its genera exist: V*x*, V*y*, V*z*', V*xy*, V*xz*', V*yz*' — and moreover the indeterminate something V exists (the wholly unspecific concept)."
 
-2. **Нисходящая ложь (очевидный).** "Если не существует род V'xy', то не существуют никакие его виды, например, V'xy'z, V'xy'z' "
+2. **Downward falsity (obvious).** "If the genus V'*xy*' does not exist, then none of its species exist either, for example V'*xy*'*z* and V'*xy*'*z*'."
 
-3. **Нисходящая истина (новый).** "Если существует род Vx и не существует вид V'xy', значит, гарантированно существует дополняющий до рода отсутствующий вид Vxy"
+3. **Downward truth (new).** "If the genus V*x* exists and the species V'*xy*' does not, then the missing species V*xy* that completes the genus is guaranteed to exist."
 
-4. **Восходящая ложь (новый).** "Если оба вида не существуют V'xy' и V'xy, значит, не существует и рода V'x"
+4. **Upward falsity (new).** "If both species fail to exist, V'*xy*' and V'*xy*, then the genus V'*x* does not exist either."
 
-Исполняя эти правила над уже известными фактами до тех пор, пока создаётся какая-то информация ("очевидная" либо "новая"), в конечном итоге мы получаем все существующие логические отношения в системе понятий.
+Applying these rules to the already known facts for as long as any information ("obvious" or "new") keeps being produced, we eventually obtain every logical relation that holds in the system of concepts.
 
-## О категорических силлогизмах Аристотеля
+## On Aristotle's categorical syllogisms
 
-Для традиционных категорических силлогизмов Аристотеля и отношения следования в естественноязыковом смысле этого слова также следует добавлять условие, что любое элементарное понятие не пусто и не полно, то есть, что по всем понятиям *x*, *y*, *z* выполняется VxVx'VyVy'VzVz' ...
\ No newline at end of file
+For Aristotle's traditional categorical syllogisms — and for entailment in the natural-language sense of the word — one must additionally require that every elementary concept is neither empty nor total, that is, that V*x*V*x*'V*y*V*y*'V*z*V*z*' … holds for all concepts *x*, *y*, *z*, …
+
+This is what the `--aristotle` flag does (see below).
+
+## Building
+
+The project is plain GHC with no external dependencies; `shell.nix` provides a suitable environment.
+
+```sh
+nix-shell            # optional, if you use Nix
+ghc -o solver Main.hs
+```
+
+To build the syllogism test runner, compile `Tests/Test.hs` from the project root (it imports the `Ternary.*` modules) and feed it `Tests/syllotest`:
+
+```sh
+ghc -i. -o syllotest Tests/Test.hs
+./syllotest < Tests/syllotest
+```
+
+## Usage
+
+```
+solver [PARAMETERS]
+```
+
+Statements are read from **standard input**, one per line, and results are written to standard output.
+
+| Parameter | Meaning |
+| --- | --- |
+| `-A`, `--aristotle` | Use the Aristotelian universe: assume V*x*V*x*' for every concept *x* mentioned in the input (no concept is empty or total). |
+| `-n`, `--new` | Print only "new" facts, omitting those that were given in the input. |
+| `--prove` | Proof mode: check whether the first input line follows from the remaining ones. |
+| `-h`, `--help` | Show the built-in help. |
+| `-v`, `--version` | Show the version. |
+
+Parameters are checked in the order `--help`, `--version`, `--prove`, then normal solving. Note that `--prove` always runs with the Aristotelian universe and ignores `-A` and `-n`.
+
+### Input format
+
+Each line is a Haskell-readable value of type `Statement String`:
+
+```
+Statement KIND "subject" "predicate"
+```
+
+Both terms must be quoted. `KIND` is one of the eight traditional forms — `A`, `E`, `I`, `O` and their primed variants `A'`, `E'`, `I'`, `O'`, in which the *first* term is negated:
+
+| Kind | Reads as | Equivalent fact |
+| --- | --- | --- |
+| `A x y` | Every *x* is *y* | V'*xy*' |
+| `E x y` | No *x* is *y* | V'*xy* |
+| `I x y` | Some *x* is *y* | V*xy* |
+| `O x y` | Some *x* is not *y* | V*xy*' |
+| `A' x y` | Every non-*x* is *y* | V'*x*'*y*' |
+| `E' x y` | No non-*x* is *y* | V'*x*'*y* |
+| `I' x y` | Some non-*x* is *y* | V*x*'*y* |
+| `O' x y` | Some non-*x* is not *y* | V*x*'*y*' |
+
+A statement that would place a term and its own negation under the same V — such as `Statement A "x" "x"` — is rejected with an error.
+
+### Output format
+
+Facts are printed in Brusentsov's notation, with a **backtick** standing for negation (the `'` used in the prose above):
+
+- `Vxy` — there exists an object that is both *x* and *y*;
+- `` V`xy` `` — there exists no object that is *x* but not *y* (i.e. every *x* is *y*);
+- a backtick immediately after `V` negates the whole set-wide disjunction; a backtick after a term name negates that term.
+
+### Example: solving
+
+```sh
+$ printf 'Statement A "man" "mortal"\nStatement A "Socrates" "man"\n' | ./solver
+V`manmortal`
+V`Socratesman`
+V`mortal`Socrates
+```
+
+The third line is the conclusion of the syllogism *Barbara*: there is no non-mortal Socrates — that is, Socrates is mortal.
+
+With the Aristotelian universe and only the newly derived facts:
+
+```sh
+$ printf 'Statement A "man" "mortal"\nStatement A "Socrates" "man"\n' | ./solver -A -n
+V`mortal`Socrates
+VmortalmanSocrates
+VSocrates`man`mortal`
+```
+
+### Example: proving
+
+In `--prove` mode the **first** line is the statement to be proved and the remaining lines are the premises. Three blocks are printed, separated by blank lines: the knowledge derived from the premises *together with* the statement, the knowledge derived from the premises alone, and the verdict.
+
+```sh
+$ printf 'Statement A "Socrates" "mortal"\nStatement A "man" "mortal"\nStatement A "Socrates" "man"\n' | ./solver --prove
+[V`Socratesmortal`,V`manmortal`,V`Socratesman`,VmortalmanSocrates,VSocrates`man`mortal`]
+
+[V`manmortal`,V`Socratesman`,V`mortal`Socrates,VmortalmanSocrates,VSocrates`man`mortal`]
+
+Just True
+```
+
+The verdict is one of:
+
+| Verdict | Meaning |
+| --- | --- |
+| `Just True` | The statement follows from the premises — adding it yields no new knowledge. |
+| `Just False` | The statement contradicts the premises. |
+| `Nothing` | Undetermined: the statement neither follows from nor contradicts the premises. |