diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index fc4966fe2..e51f1fd80 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -349,6 +349,8 @@ add_subdirectory(library/definitional)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:definitional>)
 add_subdirectory(library/blast)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast>)
+add_subdirectory(library/blast/backward)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:backward>)
 add_subdirectory(library/error_handling)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:error_handling>)
 add_subdirectory(compiler)
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 3112edc06..e4264728f 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -46,8 +46,8 @@
 (defconst lean-constants-regexp (regexp-opt lean-constants))
 (defconst lean-numerals-regexp
   (eval `(rx word-start
-	     (one-or-more digit) (optional (and "." (zero-or-more digit)))
-	     word-end)))
+             (one-or-more digit) (optional (and "." (zero-or-more digit)))
+             word-end)))
 
 (defconst lean-modifiers
   (--map (s-concat "[" it "]")
@@ -55,7 +55,7 @@
            "class" "parsing_only" "coercion" "unfold_full" "constructor"
            "reducible" "irreducible" "semireducible" "quasireducible" "wf"
            "whnf" "multiple_instances" "none" "decls" "declarations"
-           "coercions" "classes" "symm" "subst" "refl" "trans" "simp" "congr"
+           "coercions" "classes" "symm" "subst" "refl" "trans" "simp" "congr" "backward"
            "notations" "abbreviations" "begin_end_hints" "tactic_hints"
            "reduce_hints" "unfold_hints" "aliases" "eqv"
            "localrefinfo" "recursor"))
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 9f2289a90..0c7b4abaa 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -48,6 +48,7 @@ Author: Leonardo de Moura
 #include "library/simplifier/simp_rule_set.h"
 #include "library/blast/blast.h"
 #include "library/blast/simplifier.h"
+#include "library/blast/backward/backward_rule_set.h"
 #include "compiler/preprocess_rec.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/parser.h"
@@ -257,6 +258,8 @@ static void print_attributes(parser const & p, name const & n) {
         out << " [simp]";
     if (is_congr_rule(env, n))
         out << " [congr]";
+    if (is_backward_rule(env, n))
+        out << " [backward]";
     switch (get_reducible_status(env, n)) {
     case reducible_status::Reducible:      out << " [reducible]"; break;
     case reducible_status::Irreducible:    out << " [irreducible]"; break;
@@ -496,6 +499,12 @@ static void print_congr_rules(parser & p) {
     out << s.pp_congr(out.get_formatter());
 }
 
+static void print_backward_rules(parser & p) {
+    io_state_stream out = p.regular_stream();
+    blast::backward_rule_set brs = get_backward_rule_set(p.env());
+    out << brs;
+}
+
 environment print_cmd(parser & p) {
     flycheck_information info(p.regular_stream());
     if (info.enabled()) {
@@ -609,6 +618,9 @@ environment print_cmd(parser & p) {
     } else if (p.curr_is_token(get_congr_attr_tk())) {
         p.next();
         print_congr_rules(p);
+    } else if (p.curr_is_token(get_backward_attr_tk())) {
+        p.next();
+        print_backward_rules(p);
     } else if (print_polymorphic(p)) {
     } else {
         throw parser_error("invalid print command", p.pos());
diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp
index 0c8091e3f..70daaef5c 100644
--- a/src/frontends/lean/decl_attributes.cpp
+++ b/src/frontends/lean/decl_attributes.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/user_recursors.h"
 #include "library/coercion.h"
 #include "library/simplifier/simp_rule_set.h"
+#include "library/blast/backward/backward_rule_set.h"
 #include "frontends/lean/decl_attributes.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
@@ -41,6 +42,7 @@ decl_attributes::decl_attributes(bool is_abbrev, bool persistent):
     m_recursor               = false;
     m_simp                   = false;
     m_congr                  = false;
+    m_backward               = false;
 }
 
 void decl_attributes::parse(parser & p) {
@@ -87,8 +89,8 @@ void decl_attributes::parse(parser & p) {
             p.next();
         } else if (auto it = parse_priority(p)) {
             m_priority = *it;
-            if (!m_is_instance && !m_simp && !m_congr) {
-                throw parser_error("invalid '[priority]' attribute, declaration must be marked as an '[instance]', '[simp]' or '[congr]'", pos);
+            if (!m_is_instance && !m_simp && !m_congr && !m_backward) {
+                throw parser_error("invalid '[priority]' attribute, declaration must be marked as an '[instance]', '[simp]', '[congr], or [backward]'", pos);
             }
         } else if (p.curr_is_token(get_parsing_only_tk())) {
             if (!m_is_abbrev)
@@ -133,6 +135,9 @@ void decl_attributes::parse(parser & p) {
         } else if (p.curr_is_token(get_congr_attr_tk())) {
             p.next();
             m_congr = true;
+        } else if (p.curr_is_token(get_backward_attr_tk())) {
+            p.next();
+            m_backward = true;
         } else if (p.curr_is_token(get_recursor_tk())) {
             p.next();
             if (!p.curr_is_token(get_rbracket_tk())) {
@@ -213,6 +218,12 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
         else
             env = add_congr_rule(env, d, LEAN_SIMP_DEFAULT_PRIORITY, m_persistent);
     }
+    if (m_backward) {
+        if (m_priority)
+            env = add_backward_rule(env, d, *m_priority, m_persistent);
+        else
+            env = add_backward_rule(env, d, LEAN_BACKWARD_DEFAULT_PRIORITY, m_persistent);
+    }
     if (m_has_multiple_instances)
         env = mark_multiple_instances(env, d, m_persistent);
     return env;
diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h
index d12e811ff..d5d874d06 100644
--- a/src/frontends/lean/decl_attributes.h
+++ b/src/frontends/lean/decl_attributes.h
@@ -31,6 +31,7 @@ class decl_attributes {
     bool               m_recursor;
     bool               m_simp;
     bool               m_congr;
+    bool               m_backward;
     optional<unsigned> m_recursor_major_pos;
     optional<unsigned> m_priority;
     list<unsigned>     m_unfold_hint;
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 421fa67a0..83aebb2f3 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -110,7 +110,7 @@ void init_token_table(token_table & t) {
          "[persistent]", "[visible]", "[instance]", "[trans_instance]",
          "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
          "[simp]", "[congr]", "[parsing_only]", "[multiple_instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor",
-         "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold_full]", "[unfold_hints]",
+         "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold_full]", "[unfold_hints]", "[backward]",
          "[constructor]", "[unfold", "print",
          "end", "namespace", "section", "prelude", "help",
          "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index fdc1072b4..8f27100e3 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -120,6 +120,7 @@ static name const * g_refl_tk = nullptr;
 static name const * g_subst_tk = nullptr;
 static name const * g_simp_attr_tk = nullptr;
 static name const * g_congr_attr_tk = nullptr;
+static name const * g_backward_attr_tk = nullptr;
 static name const * g_recursor_tk = nullptr;
 static name const * g_attribute_tk = nullptr;
 static name const * g_with_tk = nullptr;
@@ -274,6 +275,7 @@ void initialize_tokens() {
     g_subst_tk = new name{"[subst]"};
     g_simp_attr_tk = new name{"[simp]"};
     g_congr_attr_tk = new name{"[congr]"};
+    g_backward_attr_tk = new name{"[backward]"};
     g_recursor_tk = new name{"[recursor"};
     g_attribute_tk = new name{"attribute"};
     g_with_tk = new name{"with"};
@@ -429,6 +431,7 @@ void finalize_tokens() {
     delete g_subst_tk;
     delete g_simp_attr_tk;
     delete g_congr_attr_tk;
+    delete g_backward_attr_tk;
     delete g_recursor_tk;
     delete g_attribute_tk;
     delete g_with_tk;
@@ -583,6 +586,7 @@ name const & get_refl_tk() { return *g_refl_tk; }
 name const & get_subst_tk() { return *g_subst_tk; }
 name const & get_simp_attr_tk() { return *g_simp_attr_tk; }
 name const & get_congr_attr_tk() { return *g_congr_attr_tk; }
+name const & get_backward_attr_tk() { return *g_backward_attr_tk; }
 name const & get_recursor_tk() { return *g_recursor_tk; }
 name const & get_attribute_tk() { return *g_attribute_tk; }
 name const & get_with_tk() { return *g_with_tk; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 2a16f513e..6d026d145 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -122,6 +122,7 @@ name const & get_refl_tk();
 name const & get_subst_tk();
 name const & get_simp_attr_tk();
 name const & get_congr_attr_tk();
+name const & get_backward_attr_tk();
 name const & get_recursor_tk();
 name const & get_attribute_tk();
 name const & get_with_tk();
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index fede36aa2..e8ad550ca 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -115,6 +115,7 @@ refl         [refl]
 subst        [subst]
 simp_attr    [simp]
 congr_attr   [congr]
+backward_attr [backward]
 recursor     [recursor
 attribute    attribute
 with         with
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 0832d5bf9..0a23c4ad3 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -666,6 +666,21 @@ unsigned hash_bi(expr const & e) {
     return h;
 }
 
+std::ostream & operator<<(std::ostream & out, expr_kind const & k) {
+    switch (k) {
+    case expr_kind::Var:      out << "Var"; break;
+    case expr_kind::Sort:     out << "Sort"; break;
+    case expr_kind::Constant: out << "Constant"; break;
+    case expr_kind::Meta:     out << "Meta"; break;
+    case expr_kind::Local:    out << "Local"; break;
+    case expr_kind::App:      out << "App"; break;
+    case expr_kind::Lambda:   out << "Lambda"; break;
+    case expr_kind::Pi:       out << "Pi"; break;
+    case expr_kind::Macro:    out << "Macro"; break;
+    }
+    return out;
+}
+
 void initialize_expr() {
     g_dummy        = new expr(mk_constant("__expr_for_default_constructor__"));
     g_default_name = new name("a");
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index d148ab433..36d51862d 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -617,6 +617,7 @@ expr infer_implicit(expr const & t, unsigned num_params, bool strict);
 expr infer_implicit(expr const & t, bool strict);
 // =======================================
 
+std::ostream & operator<<(std::ostream & out, expr_kind const & k);
 std::ostream & operator<<(std::ostream & out, expr const & e);
 
 void initialize_expr();
diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt
index e589feb4a..dc14fb18e 100644
--- a/src/library/blast/CMakeLists.txt
+++ b/src/library/blast/CMakeLists.txt
@@ -1,6 +1,6 @@
 add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp
   init_module.cpp simplifier.cpp simple_actions.cpp intros_action.cpp proof_expr.cpp
-  options.cpp choice_point.cpp simple_strategy.cpp backward_action.cpp util.cpp
+  options.cpp choice_point.cpp simple_strategy.cpp util.cpp
   gexpr.cpp revert.cpp subst_action.cpp no_confusion_action.cpp
   simplify_actions.cpp strategy.cpp recursor_action.cpp congruence_closure.cpp
   trace.cpp)
diff --git a/src/library/blast/backward/CMakeLists.txt b/src/library/blast/backward/CMakeLists.txt
new file mode 100644
index 000000000..dcd1994c4
--- /dev/null
+++ b/src/library/blast/backward/CMakeLists.txt
@@ -0,0 +1 @@
+add_library(backward OBJECT init_module.cpp backward_action.cpp backward_rule_set.cpp backward_strategy.cpp)
diff --git a/src/library/blast/backward_action.cpp b/src/library/blast/backward/backward_action.cpp
similarity index 100%
rename from src/library/blast/backward_action.cpp
rename to src/library/blast/backward/backward_action.cpp
diff --git a/src/library/blast/backward_action.h b/src/library/blast/backward/backward_action.h
similarity index 100%
rename from src/library/blast/backward_action.h
rename to src/library/blast/backward/backward_action.h
diff --git a/src/library/blast/backward/backward_rule_set.cpp b/src/library/blast/backward/backward_rule_set.cpp
new file mode 100644
index 000000000..9b038b892
--- /dev/null
+++ b/src/library/blast/backward/backward_rule_set.cpp
@@ -0,0 +1,161 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#include "library/blast/backward/backward_rule_set.h"
+#include "util/sstream.h"
+#include "kernel/error_msgs.h"
+#include "kernel/instantiate.h"
+#include "library/scoped_ext.h"
+#include <string>
+
+namespace lean {
+
+using blast::backward_rule;
+using blast::backward_rule_set;
+using blast::gexpr;
+
+static name * g_class_name = nullptr;
+static std::string * g_key = nullptr;
+
+struct brs_state {
+    backward_rule_set        m_backward_rule_set;
+    name_set                 m_names;
+    void add(environment const & env, io_state const & ios, name const & cname, unsigned prio) {
+        default_type_context tctx(env, ios);
+        m_backward_rule_set.insert(tctx, cname, prio);
+        m_names.insert(cname);
+    }
+};
+
+struct brs_entry {
+    name     m_name;
+    unsigned m_priority;
+    brs_entry() {}
+    brs_entry(name const & n, unsigned prio): m_name(n), m_priority(prio) { }
+};
+
+struct brs_config {
+    typedef brs_entry  entry;
+    typedef brs_state  state;
+    static void add_entry(environment const & env, io_state const & ios, state & s, entry const & e) {
+        s.add(env, ios, e.m_name, e.m_priority);
+    }
+    static name const & get_class_name() {
+        return *g_class_name;
+    }
+    static std::string const & get_serialization_key() {
+        return *g_key;
+    }
+    static void  write_entry(serializer & s, entry const & e) {
+        s << e.m_name << e.m_priority;
+    }
+    static entry read_entry(deserializer & d) {
+        entry e; d >> e.m_name >> e.m_priority; return e;
+    }
+    static optional<unsigned> get_fingerprint(entry const & e) {
+        return some(e.m_name.hash());
+    }
+};
+
+template class scoped_ext<brs_config>;
+typedef scoped_ext<brs_config> brs_ext;
+
+environment add_backward_rule(environment const & env, name const & n, unsigned priority,  bool persistent) {
+    return brs_ext::add_entry(env, get_dummy_ios(), brs_entry(n, priority), persistent);
+}
+
+bool is_backward_rule(environment const & env, name const & n) {
+    return brs_ext::get_state(env).m_names.contains(n);
+}
+
+backward_rule_set get_backward_rule_set(environment const & env) {
+    return brs_ext::get_state(env).m_backward_rule_set;
+}
+
+backward_rule_set get_backward_rule_sets(environment const & env, io_state const & ios, name const & ns) {
+    backward_rule_set brs;
+    list<brs_entry> const * entries = brs_ext::get_entries(env, ns);
+    if (entries) {
+        for (auto const & e : *entries) {
+            default_type_context tctx(env, ios);
+            brs.insert(tctx, e.m_name, e.m_priority);
+        }
+    }
+    return brs;
+}
+
+io_state_stream const & operator<<(io_state_stream const & out, backward_rule_set const & brs) {
+    options const & opts = out.get_options();
+    out << "backward rules\n";
+    brs.for_each([&](head_index const & head_idx, backward_rule const & r) {
+            out << head_idx << " ==> " << r.get_proof() << "\n";
+        });
+    return out;
+}
+
+namespace blast {
+
+bool operator==(backward_rule const & r1, backward_rule const & r2) {
+    return r1.get_proof() == r2.get_proof();
+}
+
+void backward_rule_set::insert(type_context & tctx, name const & id, gexpr const & proof, expr const & _thm, unsigned prio) {
+    expr thm = tctx.whnf(_thm);
+    while (is_pi(thm)) {
+        expr local = tctx.mk_tmp_local(binding_domain(thm), binding_info(thm));
+        thm = tctx.whnf(instantiate(binding_body(thm), local));
+    }
+    m_set.insert(head_index(thm), backward_rule(id, proof, prio));
+}
+
+void backward_rule_set::insert(type_context & tctx, name const & name, unsigned prio) {
+    gexpr proof(tctx.env(), name);
+    declaration const & d = tctx.env().get(name);
+    insert(tctx, name, proof, d.get_type(), prio);
+}
+
+void backward_rule_set::erase(name_set const & ids) {
+    // This method is not very smart and doesn't use any indexing or caching.
+    // So, it may be a bottleneck in the future
+    buffer<pair<head_index, backward_rule> > to_delete;
+    for_each([&](head_index const & h, backward_rule const & r) {
+            if (ids.contains(r.get_id())) {
+                to_delete.push_back(mk_pair(h, r));
+            }
+        });
+    for (auto const & hr : to_delete) {
+        m_set.erase(hr.first, hr.second);
+    }
+}
+
+void backward_rule_set::erase(name const & id) {
+    name_set ids;
+    ids.insert(id);
+    erase(ids);
+}
+
+void backward_rule_set::for_each(std::function<void(head_index const & h, backward_rule const & r)> const & fn) const {
+    m_set.for_each_entry(fn);
+}
+
+list<gexpr> backward_rule_set::find(head_index const & h) const {
+    list<backward_rule> const * rule_list = m_set.find(h);
+    if (!rule_list) return list<gexpr>();
+    return map2<gexpr>(*rule_list, [&](backward_rule const & r) { return r.get_proof(); });
+}
+
+void initialize_backward_rule_set() {
+    g_class_name = new name("brs");
+    g_key        = new std::string("brs");
+    brs_ext::initialize();
+}
+
+void finalize_backward_rule_set() {
+    brs_ext::finalize();
+    delete g_key;
+    delete g_class_name;
+}
+}
+}
diff --git a/src/library/blast/backward/backward_rule_set.h b/src/library/blast/backward/backward_rule_set.h
new file mode 100644
index 000000000..6c27166b0
--- /dev/null
+++ b/src/library/blast/backward/backward_rule_set.h
@@ -0,0 +1,68 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#pragma once
+#include "library/type_context.h"
+#include "library/head_map.h"
+#include "library/io_state_stream.h"
+#include "library/blast/gexpr.h"
+#include <vector>
+
+#ifndef LEAN_BACKWARD_DEFAULT_PRIORITY
+#define LEAN_BACKWARD_DEFAULT_PRIORITY 1000
+#endif
+
+namespace lean {
+namespace blast {
+
+class backward_rule {
+    name            m_id;
+    gexpr           m_proof;
+    unsigned        m_priority;
+
+public:
+    backward_rule(name const & id, gexpr const & proof, unsigned priority):
+        m_id(id), m_proof(proof), m_priority(priority) {}
+
+    name const & get_id() const { return m_id; }
+    gexpr const & get_proof() const { return m_proof; }
+    unsigned get_priority() const { return m_priority; }
+};
+
+bool operator==(backward_rule const & r1, backward_rule const & r2);
+inline bool operator!=(backward_rule const & r1, backward_rule const & r2) { return !operator==(r1, r2); }
+
+struct backward_rule_prio_fn { unsigned operator()(backward_rule const & r) const { return r.get_priority(); } };
+
+class backward_rule_set {
+    head_map_prio<backward_rule, backward_rule_prio_fn> m_set;
+
+public:
+    void insert(type_context & tctx, name const & id, gexpr const & proof, expr const & thm, unsigned prio);
+    void insert(type_context & tctx, name const & name, unsigned prio);
+    void erase(name_set const & ids);
+    void erase(name const & id);
+    void for_each(std::function<void(head_index const & h, backward_rule const & r)> const & fn) const;
+    list<gexpr> find(head_index const & h) const;
+};
+
+
+void initialize_backward_rule_set();
+void finalize_backward_rule_set();
+}
+
+environment add_backward_rule(environment const & env, name const & n, unsigned priority, bool persistent);
+
+/** \brief Return true if \c n is an active backward rule in \c env */
+bool is_backward_rule(environment const & env, name const & n);
+
+/** \brief Get current backward rule set */
+blast::backward_rule_set get_backward_rule_set(environment const & env);
+/** \brief Get backward rule set in the given namespace. */
+blast::backward_rule_set get_backward_rule_sets(environment const & env, io_state const & ios, name const & ns);
+
+io_state_stream const & operator<<(io_state_stream const & out, blast::backward_rule_set const & r);
+
+}
diff --git a/src/library/blast/backward/backward_strategy.cpp b/src/library/blast/backward/backward_strategy.cpp
new file mode 100644
index 000000000..75d4d7d3f
--- /dev/null
+++ b/src/library/blast/backward/backward_strategy.cpp
@@ -0,0 +1,81 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#include "library/blast/blast.h"
+#include "library/blast/trace.h"
+#include "library/blast/options.h"
+#include "library/blast/choice_point.h"
+#include "library/blast/simple_actions.h"
+#include "library/blast/proof_expr.h"
+#include "library/blast/intros_action.h"
+#include "library/blast/no_confusion_action.h"
+#include "library/blast/subst_action.h"
+#include "library/blast/backward/backward_rule_set.h"
+#include "library/blast/backward/backward_action.h"
+#include "library/blast/strategy.h"
+
+namespace lean {
+namespace blast {
+static unsigned g_ext_id = 0;
+struct backward_branch_extension : public branch_extension {
+    backward_rule_set m_backward_rule_set;
+    backward_branch_extension() {}
+    backward_branch_extension(backward_branch_extension const & b):
+        m_backward_rule_set(b.m_backward_rule_set) {}
+    virtual ~backward_branch_extension() {}
+    virtual branch_extension * clone() override { return new backward_branch_extension(*this); }
+    virtual void initialized() override { m_backward_rule_set = ::lean::get_backward_rule_set(env()); }
+    virtual void hypothesis_activated(hypothesis const & h, hypothesis_idx hidx) override {
+        m_backward_rule_set.insert(get_type_context(), h.get_name(), gexpr(mk_href(hidx)),
+                                   h.get_type(), LEAN_BACKWARD_DEFAULT_PRIORITY);
+    }
+    virtual void hypothesis_deleted(hypothesis const & h, hypothesis_idx) override {
+        m_backward_rule_set.erase(h.get_name());
+    }
+    backward_rule_set const & get_backward_rule_set() const { return m_backward_rule_set; }
+};
+
+void initialize_backward_strategy() {
+    g_ext_id = register_branch_extension(new backward_branch_extension());
+}
+
+void finalize_backward_strategy() {
+}
+
+static backward_branch_extension & get_extension() {
+    return static_cast<backward_branch_extension&>(curr_state().get_extension(g_ext_id));
+}
+
+/** \brief Basic backwards chaining, inspired by Coq's [auto]. */
+class backward_strategy : public strategy {
+    virtual optional<expr> preprocess() override { return none_expr(); }
+
+    action_result activate_hypothesis() {
+        optional<hypothesis_idx> hidx = curr_state().activate_hypothesis();
+        if (!hidx) return action_result::failed();
+        trace_action("activate");
+
+        Try(assumption_contradiction_actions(*hidx));
+        Try(subst_action(*hidx));
+        Try(no_confusion_action(*hidx));
+        Try(discard_action(*hidx));
+        return action_result::new_branch();
+    }
+
+    virtual action_result next_action() override {
+        Try(intros_action());
+        Try(activate_hypothesis());
+        Try(trivial_action());
+        Try(assumption_action());
+        list<gexpr> backward_rules = get_extension().get_backward_rule_set().find(head_index(curr_state().get_target()));
+        Try(backward_action(backward_rules, true));
+        return action_result::failed();
+    }
+};
+
+optional<expr> apply_backward_strategy() {
+    return backward_strategy()();
+}
+}}
diff --git a/src/library/blast/backward/backward_strategy.h b/src/library/blast/backward/backward_strategy.h
new file mode 100644
index 000000000..0085982c2
--- /dev/null
+++ b/src/library/blast/backward/backward_strategy.h
@@ -0,0 +1,15 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#pragma once
+#include "kernel/expr.h"
+
+namespace lean {
+namespace blast {
+optional<expr> apply_backward_strategy();
+
+void initialize_backward_strategy();
+void finalize_backward_strategy();
+}}
diff --git a/src/library/blast/backward/init_module.cpp b/src/library/blast/backward/init_module.cpp
new file mode 100644
index 000000000..7391f0c1d
--- /dev/null
+++ b/src/library/blast/backward/init_module.cpp
@@ -0,0 +1,23 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#include "library/blast/backward/init_module.h"
+#include "library/blast/backward/backward_rule_set.h"
+#include "library/blast/backward/backward_strategy.h"
+
+namespace lean {
+namespace blast {
+
+void initialize_backward_module() {
+    initialize_backward_rule_set();
+    initialize_backward_strategy();
+}
+
+void finalize_backward_module() {
+    finalize_backward_strategy();
+    finalize_backward_rule_set();
+}
+}
+}
diff --git a/src/library/blast/backward/init_module.h b/src/library/blast/backward/init_module.h
new file mode 100644
index 000000000..ac97b7dcb
--- /dev/null
+++ b/src/library/blast/backward/init_module.h
@@ -0,0 +1,13 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#pragma once
+
+namespace lean {
+namespace blast {
+void initialize_backward_module();
+void finalize_backward_module();
+}
+}
diff --git a/src/library/blast/gexpr.cpp b/src/library/blast/gexpr.cpp
index ecfa02a90..768cb8581 100644
--- a/src/library/blast/gexpr.cpp
+++ b/src/library/blast/gexpr.cpp
@@ -26,4 +26,13 @@ expr gexpr::to_expr(type_context & ctx) const {
 expr gexpr::to_expr() const {
     return to_expr(get_type_context());
 }
+
+bool operator==(gexpr const & ge1, gexpr const & ge2) { return ge1.m_expr == ge2.m_expr; }
+
+std::ostream & operator<<(std::ostream & out, gexpr const & ge) {
+    out << ge.m_expr;
+    if (ge.is_universe_polymorphic()) out << " (poly)";
+    return out;
+}
+
 }}
diff --git a/src/library/blast/gexpr.h b/src/library/blast/gexpr.h
index bf3be1477..9d82e1730 100644
--- a/src/library/blast/gexpr.h
+++ b/src/library/blast/gexpr.h
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/expr.h"
 #include "library/type_context.h"
+#include "library/io_state_stream.h"
 
 namespace lean {
 namespace blast {
@@ -25,6 +26,8 @@ struct gexpr {
 public:
     gexpr(name const & n):m_univ_poly(true), m_expr(mk_constant(n)) {}
     gexpr(expr const & e):m_univ_poly(false), m_expr(e) {}
+    gexpr(environment const & env, name const & n):
+        m_univ_poly(env.get(n).get_univ_params()), m_expr(mk_constant(n)) {}
 
     bool is_universe_polymorphic() const {
         return m_univ_poly;
@@ -38,5 +41,13 @@ public:
     /** \brief Similar to previous method, but uses \c mk_fresh_uref to
         create fresh universe meta-variables */
     expr to_expr() const;
+
+    friend bool operator==(gexpr const & ge1, gexpr const & ge2);
+    friend std::ostream const & operator<<(std::ostream const & out, gexpr const & ge);
 };
+
+bool operator==(gexpr const & ge1, gexpr const & ge2);
+inline bool operator!=(gexpr const & ge1, gexpr const & ge2) { return !operator==(ge1, ge2); }
+std::ostream & operator<<(std::ostream & out, gexpr const & ge);
+
 }}
diff --git a/src/library/blast/init_module.cpp b/src/library/blast/init_module.cpp
index 2605a072d..6674434f3 100644
--- a/src/library/blast/init_module.cpp
+++ b/src/library/blast/init_module.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/blast/simplifier.h"
 #include "library/blast/options.h"
 #include "library/blast/recursor_action.h"
+#include "library/blast/backward/init_module.h"
 
 namespace lean {
 void initialize_blast_module() {
@@ -19,12 +20,14 @@ void initialize_blast_module() {
     blast::initialize_state();
     initialize_blast();
     blast::initialize_simplifier();
+    blast::initialize_backward_module();
     initialize_blast_tactic();
     blast::initialize_recursor_action();
 }
 void finalize_blast_module() {
     blast::finalize_recursor_action();
     finalize_blast_tactic();
+    blast::finalize_backward_module();
     blast::finalize_simplifier();
     finalize_blast();
     blast::finalize_state();
diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp
index 5288fd437..9c0c3fe4f 100644
--- a/src/library/blast/simple_strategy.cpp
+++ b/src/library/blast/simple_strategy.cpp
@@ -11,7 +11,8 @@ Author: Leonardo de Moura
 #include "library/blast/proof_expr.h"
 #include "library/blast/intros_action.h"
 #include "library/blast/subst_action.h"
-#include "library/blast/backward_action.h"
+#include "library/blast/backward/backward_action.h"
+#include "library/blast/backward/backward_strategy.h"
 #include "library/blast/no_confusion_action.h"
 #include "library/blast/simplify_actions.h"
 #include "library/blast/recursor_action.h"
@@ -43,6 +44,10 @@ class simple_strategy : public strategy {
        Return an expression if the goal has been proved during preprocessing step. */
     virtual optional<expr> preprocess() {
         trace("* Preprocess");
+
+        // TODO(dhs): make a branch extension
+        curr_state().set_simp_rule_sets(get_simp_rule_sets(env()));
+
         while (true) {
             if (!failed(intros_action()))
                 continue;
@@ -62,6 +67,11 @@ class simple_strategy : public strategy {
         Try(assumption_action());
         Try(recursor_action());
         Try(constructor_action());
+
+        TryStrategy(apply_backward_strategy());
+
+        // TODO(Leo): add more actions...
+
         return action_result::failed();
     }
 };
diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp
index af45c44ae..41d12514e 100644
--- a/src/library/blast/state.cpp
+++ b/src/library/blast/state.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 #include "library/replace_visitor.h"
 #include "library/blast/util.h"
+#include "library/blast/blast.h"
 #include "library/blast/state.h"
 
 namespace lean {
diff --git a/src/library/blast/state.h b/src/library/blast/state.h
index 2b0e33b23..ef4b9f924 100644
--- a/src/library/blast/state.h
+++ b/src/library/blast/state.h
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/head_map.h"
 #include "library/tactic/goal.h"
 #include "library/simplifier/simp_rule_set.h"
+#include "library/blast/backward/backward_rule_set.h"
 #include "library/blast/action_result.h"
 #include "library/blast/hypothesis.h"
 
diff --git a/src/library/blast/strategy.cpp b/src/library/blast/strategy.cpp
index e26a1f53c..774463ab6 100644
--- a/src/library/blast/strategy.cpp
+++ b/src/library/blast/strategy.cpp
@@ -92,7 +92,6 @@ optional<expr> strategy::search() {
     scope_choice_points scope1;
     curr_state().clear_proof_steps();
     m_init_num_choices = get_num_choice_points();
-    curr_state().set_simp_rule_sets(get_simp_rule_sets(env()));
     if (auto pr = invoke_preprocess())
         return pr;
     if (get_num_choice_points() > m_init_num_choices)
diff --git a/src/library/blast/strategy.h b/src/library/blast/strategy.h
index 3d278f408..7bd377092 100644
--- a/src/library/blast/strategy.h
+++ b/src/library/blast/strategy.h
@@ -7,6 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 #include "library/blast/action_result.h"
 #include "library/blast/options.h"
+#include "library/blast/blast.h"
+#include "util/flet.h"
 
 namespace lean {
 namespace blast {
@@ -31,4 +33,10 @@ public:
     strategy();
     optional<expr> operator()() { return search(); }
 };
+
+#define TryStrategy(Code) {\
+        flet<state> save_state(curr_state(), curr_state());\
+        curr_state().clear_proof_steps();\
+        if (optional<expr> pf = Code) { return action_result::solved(*pf); }\
+    }
 }}
diff --git a/src/library/head_map.cpp b/src/library/head_map.cpp
index af6944e10..2cfabf592 100644
--- a/src/library/head_map.cpp
+++ b/src/library/head_map.cpp
@@ -33,4 +33,12 @@ int head_index::cmp::operator()(head_index const & i1, head_index const & i2) co
     else
         return quick_cmp(i1.m_name, i2.m_name);
 }
+
+std::ostream & operator<<(std::ostream & out, head_index const & head_idx) {
+    if (head_idx.m_kind == expr_kind::Constant || head_idx.m_kind == expr_kind::Local)
+        out << head_idx.m_name;
+    else
+        out << head_idx.m_kind;
+    return out;
+}
 }
diff --git a/src/library/head_map.h b/src/library/head_map.h
index 265bf3619..10a8bade2 100644
--- a/src/library/head_map.h
+++ b/src/library/head_map.h
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "util/rb_map.h"
 #include "util/list.h"
 #include "kernel/expr.h"
+#include "library/io_state_stream.h"
 
 namespace lean {
 struct head_index {
@@ -20,6 +21,8 @@ struct head_index {
     struct cmp {
         int operator()(head_index const & i1, head_index const & i2) const;
     };
+
+    friend std::ostream & operator<<(std::ostream & out, head_index const & head_idx);
 };
 
 /**
diff --git a/src/library/io_state_stream.cpp b/src/library/io_state_stream.cpp
index 776667d10..9c00e2106 100644
--- a/src/library/io_state_stream.cpp
+++ b/src/library/io_state_stream.cpp
@@ -14,6 +14,12 @@ io_state_stream const & operator<<(io_state_stream const & out, endl_class) {
     return out;
 }
 
+io_state_stream const & operator<<(io_state_stream const & out, expr_kind const & k) {
+    options const & opts = out.get_options();
+    out.get_stream() << k;
+    return out;
+}
+
 io_state_stream const & operator<<(io_state_stream const & out, expr const & e) {
     options const & opts = out.get_options();
     out.get_stream() << mk_pair(group(out.get_formatter()(e)), opts);
diff --git a/tests/lean/backward_rule1.lean b/tests/lean/backward_rule1.lean
new file mode 100644
index 000000000..e5e505dc9
--- /dev/null
+++ b/tests/lean/backward_rule1.lean
@@ -0,0 +1,11 @@
+constants (A B C : Prop) (H : A → B) (G : A → B → C)
+constants (T : Type) (f : T → A)
+attribute H [backward]
+attribute G [backward]
+attribute f [backward]
+
+print H
+print G
+print f
+
+print [backward]
diff --git a/tests/lean/backward_rule1.lean.expected.out b/tests/lean/backward_rule1.lean.expected.out
new file mode 100644
index 000000000..f6a4924f4
--- /dev/null
+++ b/tests/lean/backward_rule1.lean.expected.out
@@ -0,0 +1,7 @@
+constant H [backward] : A → B
+constant G [backward] : A → B → C
+constant f [backward] : T → A
+backward rules
+B ==> H
+A ==> f (poly)
+C ==> G
diff --git a/tests/lean/run/blast18.lean b/tests/lean/run/blast18.lean
new file mode 100644
index 000000000..935ad4e89
--- /dev/null
+++ b/tests/lean/run/blast18.lean
@@ -0,0 +1,17 @@
+-- Backward chaining with tagged rules
+constants {P Q R S T U : Prop} (Hpq : P → Q) (Hqr : Q → R) (Hrs : R → S) (Hst : S → T)
+constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T)
+attribute Hpq [backward]
+attribute Hqr [backward]
+attribute Hrs [backward]
+attribute Hst [backward]
+
+attribute Huq [backward]
+attribute Hur [backward]
+attribute Hus [backward]
+attribute Hut [backward]
+
+definition lemma1 (p : P) : Q := by blast
+definition lemma2 (p : P) : R := by blast
+definition lemma3 (p : P) : S := by blast
+definition lemma4 (p : P) : T := by blast
diff --git a/tests/lean/run/blast19.lean b/tests/lean/run/blast19.lean
new file mode 100644
index 000000000..08e3d07e7
--- /dev/null
+++ b/tests/lean/run/blast19.lean
@@ -0,0 +1,12 @@
+-- Backward chaining with hypotheses
+constants {P Q R S T U : Prop}
+constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T)
+attribute Huq [backward]
+attribute Hur [backward]
+attribute Hus [backward]
+attribute Hut [backward]
+
+definition lemma1 : (P → Q) → P → Q := by blast
+definition lemma2 : (P → Q) → (Q → R) → P → R := by blast
+definition lemma3 : (P → Q) → (Q → R) → (R → S) → P → S := by blast
+definition lemma4 : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by blast