diff --git a/editor/Manual.esv b/editor/Manual.esv
index fae7b1b..e91573b 100644
--- a/editor/Manual.esv
+++ b/editor/Manual.esv
@@ -1,5 +1,8 @@
 module Manual
 menus
-  menu: "Manual" (openeditor)
-   action: "prop-eval" = do-eval (source)
-   action: "prop-dnf"  = do-dnf  (source)
+  menu: "Manual" (openeditor) (source)
+    action: "prop-eval" = do-eval
+    action: "prop-dnf"  = do-dnf
+    action: "prop-dnf3" = do-dnf3
+    action: "prop-cnf3" = do-cnf3
+    action: "both nf3"  = do-dcnf
diff --git a/syntax/examples/sec5.1.2_test1.spl b/syntax/examples/sec5.1.2_test1.spl
new file mode 100644
index 0000000..cfce111
--- /dev/null
+++ b/syntax/examples/sec5.1.2_test1.spl
@@ -0,0 +1 @@
+(r -> p & q) & p
diff --git a/test/manual-suite.spt b/test/manual-suite.spt
index f8e41d0..5d22850 100644
--- a/test/manual-suite.spt
+++ b/test/manual-suite.spt
@@ -9,4 +9,19 @@ test sec4_2_test3_ex [[
   (r -> p & q) & p
 ]] run dnf to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
 
+test sec5_1_2_test1_ex [[
+  (r -> p & q) & p
+]] run dnf3 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
 
+test sec5_1_2_test1_cnf_ex [[
+  (r -> p & q) & p
+]] run cnf3 to And(And(Or(Not(Atom("r")), Atom("p")),
+                       Or(Not(Atom("r")), Atom("q"))),
+                   Atom("p"))
+
+test sec5_1_2_test1_both_ex [[
+  (r -> p & q) & p
+]] run dcnf to (Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p"))),
+                And(And(Or(Not(Atom("r")), Atom("p")),
+                        Or(Not(Atom("r")), Atom("q"))),
+                    Atom("p")))
diff --git a/trans/prop-cnf3.str b/trans/prop-cnf3.str
new file mode 100644
index 0000000..e371c74
--- /dev/null
+++ b/trans/prop-cnf3.str
@@ -0,0 +1,35 @@
+module prop-cnf3
+imports libstrategolib prop-dnf3 signatures/-
+signature
+  constructors
+    Cnf  : Prop -> Prop
+    CnfR : Prop -> Prop
+rules
+  E3 : Cnf(Atom(x))    -> Atom(x)
+  E3 : Cnf(Not(x))     -> CnfR(Not(Cnf(x)))
+  E3 : Cnf(Or(x, y))   -> CnfR(Or(Cnf(x), Cnf(y)))
+  E3 : Cnf(And(x, y))  -> And(Cnf(x), Cnf(y))
+  E3 : Cnf(Impl(x, y)) -> Cnf(Not(And(x, Not(y))))
+  E3 : Cnf(Eq(x, y))   -> Cnf(And(Impl(x, y), Impl(y, x)))
+
+  E3 : CnfR(Not(Not(x)))      -> x
+  E3 : CnfR(Not(Or(x, y)))    -> And(Cnf(Not(x)), Cnf(Not(y)))
+  E3 : CnfR(Not(And(x, y)))   -> Cnf(Or(Not(x), Not(y)))
+  D3 : CnfR(Not(x))           -> Not(x)
+
+  E3 : CnfR(Or(And(x, y), z)) -> And(Cnf(Or(x, z)), Cnf(Or(y, z)))
+  E3 : CnfR(Or(z, And(x, y))) -> And(Cnf(Or(z, x)), Cnf(Or(z, y)))
+  D3 : CnfR(Or(x, y))         -> Or(x, y)
+  
+strategies
+  cnf3 : x -> <make-nf> Cnf(x)
+  dcnf : x -> <make-nf> (Dnf(x), Cnf(x))
+  
+  // Interface cnf3 strategy with editor services and file system
+  do-cnf3: (selected, _, _, path, project-path) -> (filename, result)
+    with filename := <guarantee-extension(|"cnf.aterm")> path
+       ; result   := <cnf3> selected
+       
+  do-dcnf: (selected, _, _, path, project-path) -> (filename, result)
+    with filename := <guarantee-extension(|"dc.aterm")> path
+       ; result   := <dcnf> selected
\ No newline at end of file
diff --git a/trans/prop-dnf3.str b/trans/prop-dnf3.str
new file mode 100644
index 0000000..6583969
--- /dev/null
+++ b/trans/prop-dnf3.str
@@ -0,0 +1,31 @@
+module prop-dnf3
+imports libstrategolib signatures/-
+signature
+  constructors
+    Dnf  : Prop -> Prop
+    DnfR : Prop -> Prop
+rules
+  E3 : Dnf(Atom(x))    -> Atom(x)
+  E3 : Dnf(Not(x))     -> DnfR(Not(Dnf(x)))
+  E3 : Dnf(And(x, y))  -> DnfR(And(Dnf(x), Dnf(y)))
+  E3 : Dnf(Or(x, y))   -> Or(Dnf(x), Dnf(y))
+  E3 : Dnf(Impl(x, y)) -> Dnf(Or(Not(x), y))
+  E3 : Dnf(Eq(x, y))   -> Dnf(And(Impl(x, y), Impl(y, x)))
+
+  E3 : DnfR(Not(Not(x)))      -> x
+  E3 : DnfR(Not(And(x, y)))   -> Or(Dnf(Not(x)), Dnf(Not(y)))
+  E3 : DnfR(Not(Or(x, y)))    -> Dnf(And(Not(x), Not(y)))
+  D3 : DnfR(Not(x))           -> Not(x)
+
+  E3 : DnfR(And(Or(x, y), z)) -> Or(Dnf(And(x, z)), Dnf(And(y, z)))
+  E3 : DnfR(And(z, Or(x, y))) -> Or(Dnf(And(z, x)), Dnf(And(z, y)))
+  D3 : DnfR(And(x, y))        -> And(x, y)
+
+strategies
+  make-nf  = innermost(E3 <+ D3)
+  dnf3 : x -> <make-nf> Dnf(x)
+  
+  // Interface dnf3 strategy with editor services and file system
+  do-dnf3: (selected, _, _, path, project-path) -> (filename, result)
+    with filename := <guarantee-extension(|"dnf.aterm")> path
+       ; result   := <dnf3> selected
\ No newline at end of file
diff --git a/trans/prop-eval-rules.str b/trans/prop-eval-rules.str
index e0cd1eb..c36d88f 100644
--- a/trans/prop-eval-rules.str
+++ b/trans/prop-eval-rules.str
@@ -88,7 +88,7 @@ It's just the one line `Manual` in the `imports` section that we have added. The
 {! ../editor/Manual.esv terminate: dnf !}
 ```
 Note that the quoted string on the `action` line is the text label of the menu
-item in the "Manual" submenu, and the first identifier on its right-hand side is the
+item in the "Manual" submenu, and the identifier on its right-hand side is the
 Stratego action to call. But note that `do-eval` is not the same identifier as
 `eval` in our last Stratego file above. That's because the Stratego invocation
 caused by an ESV action item has a specific, multi-item argument list, whereas
diff --git a/trans/spoofax_propositional_language.str b/trans/spoofax_propositional_language.str
index 3374459..4452125 100644
--- a/trans/spoofax_propositional_language.str
+++ b/trans/spoofax_propositional_language.str
@@ -8,6 +8,8 @@ imports
   analysis
   prop-eval
   prop-dnf
+  prop-dnf3
+  prop-cnf3
 
 rules // Debugging