diff --git a/extra/boolean-expr/authors.txt b/extra/boolean-expr/authors.txt
new file mode 100644
index 0000000000..1901f27a24
--- /dev/null
+++ b/extra/boolean-expr/authors.txt
@@ -0,0 +1 @@
+Slava Pestov
diff --git a/extra/boolean-expr/boolean-expr.factor b/extra/boolean-expr/boolean-expr.factor
new file mode 100644
index 0000000000..b2083eed55
--- /dev/null
+++ b/extra/boolean-expr/boolean-expr.factor
@@ -0,0 +1,96 @@
+! Copyright (C) 2008 Slava Pestov.
+! See http://factorcode.org/license.txt for BSD license.
+USING: accessors arrays classes kernel sequences sets
+io prettyprint multi-methods symbols ;
+IN: boolean-expr
+
+! Demonstrates the use of Unicode symbols in source files, and
+! multi-method dispatch.
+
+TUPLE: ⋀ x y ;
+TUPLE: ⋁ x y ;
+TUPLE: ¬ x ;
+
+SINGLETON: ⊤
+SINGLETON: ⊥
+
+SINGLETONS: P Q R S T U V W X Y Z ;
+
+UNION: □ ⋀ ⋁ ¬ ⊤ ⊥ P Q R S T U V W X Y Z ;
+
+GENERIC: ⋀ ( x y -- expr )
+
+METHOD: ⋀ { ⊤ □ } nip ;
+METHOD: ⋀ { □ ⊤ } drop ;
+METHOD: ⋀ { ⊥ □ } drop ;
+METHOD: ⋀ { □ ⊥ } nip ;
+
+METHOD: ⋀ { ⋁ □ } [ [ x>> ] dip ⋀ ] [ [ y>> ] dip ⋀ ] 2bi ⋁ ;
+METHOD: ⋀ { □ ⋁ } [ x>> ⋀ ] [ y>> ⋀ ] 2bi ⋁ ;
+
+METHOD: ⋀ { □ □ } \ ⋀ boa ;
+
+GENERIC: ⋁ ( x y -- expr )
+
+METHOD: ⋁ { ⊤ □ } drop ;
+METHOD: ⋁ { □ ⊤ } nip ;
+METHOD: ⋁ { ⊥ □ } nip ;
+METHOD: ⋁ { □ ⊥ } drop ;
+
+METHOD: ⋁ { □ □ } \ ⋁ boa ;
+
+GENERIC: ¬ ( x -- expr )
+
+METHOD: ¬ { ⊤ } drop ⊥ ;
+METHOD: ¬ { ⊥ } drop ⊤ ;
+
+METHOD: ¬ { ⋀ } [ x>> ¬ ] [ y>> ¬ ] bi ⋁ ;
+METHOD: ¬ { ⋁ } [ x>> ¬ ] [ y>> ¬ ] bi ⋀ ;
+
+METHOD: ¬ { □ } \ ¬ boa ;
+
+: → ( x y -- expr ) ¬ ⋀ ;
+: ⊕ ( x y -- expr ) [ ⋁ ] [ ⋀ ¬ ] 2bi ⋀ ;
+: ≣ ( x y -- expr ) [ ⋀ ] [ [ ¬ ] bi@ ⋀ ] 2bi ⋁ ;
+
+GENERIC: (cnf) ( expr -- cnf )
+
+METHOD: (cnf) { ⋀ } [ x>> (cnf) ] [ y>> (cnf) ] bi append ;
+METHOD: (cnf) { □ } 1array ;
+
+GENERIC: cnf ( expr -- cnf )
+
+METHOD: cnf { ⋁ } [ x>> cnf ] [ y>> cnf ] bi append ;
+METHOD: cnf { □ } (cnf) 1array ;
+
+GENERIC: satisfiable? ( expr -- ? )
+
+METHOD: satisfiable? { ⊤ } drop t ;
+METHOD: satisfiable? { ⊥ } drop f ;
+
+: partition ( seq quot -- left right )
+    [ [ not ] compose filter ] [ filter ] 2bi ; inline
+
+: (satisfiable?) ( seq -- ? )
+    [ \ ¬ instance? ] partition [ x>> ] map intersect empty? ;
+
+METHOD: satisfiable? { □ }
+    cnf [ (satisfiable?) ] contains? ;
+
+GENERIC: (expr.) ( expr -- )
+
+METHOD: (expr.) { □ } pprint ;
+
+: op. ( expr -- )
+    "(" write
+    [ x>> (expr.) ]
+    [ bl class pprint bl ]
+    [ y>> (expr.) ]
+    tri
+    ")" write ;
+
+METHOD: (expr.) { ⋀ } op. ;
+METHOD: (expr.) { ⋁ } op. ;
+METHOD: (expr.) { ¬ } [ class pprint ] [ x>> (expr.) ] bi ;
+
+: expr. ( expr -- ) (expr.) nl ;
diff --git a/extra/boolean-expr/summary.txt b/extra/boolean-expr/summary.txt
new file mode 100644
index 0000000000..9b51186ca9
--- /dev/null
+++ b/extra/boolean-expr/summary.txt
@@ -0,0 +1 @@
+Simple boolean expression evaluator and simplifier
diff --git a/extra/boolean-expr/tags.txt b/extra/boolean-expr/tags.txt
new file mode 100644
index 0000000000..cb5fc203e1
--- /dev/null
+++ b/extra/boolean-expr/tags.txt
@@ -0,0 +1 @@
+demos