# Backward Chainer Experiments

## Description

Contains a number of experiments to realize backward chaining in
MeTTa.  Specifically:

* *Bare Entail*: represent rules with the `⊢` relationship.  Knowledge
  however is not wrapped around `⊢`.
* *Equality*: like bare entail but the rules are directly encoded in
  the backward chainer function.
* *Bare Entail Match*: like bare entail but both knowledge and rule
  bases are stored in their own spaces and `match` is used instead of
  `let`.  `let*` is still used to bind the and-branches of the
  inference trees together.  By and-branches we mean the multiple
  premises an inference rule must satify at once.
* *Equality Match*: like equality but the knowledge base is stored in
  its own space, the rules are directly encoded in the backward
  chainer function, and `match` is used instead of `let` to match
  premises with the knowledge base.  `let*` is still used to bind the
  and-branches of the inference trees together.
* *DTL Equality Match*: like DTL (Synthesizer) but the rules are hard
  wired in the backward chainer function and match used instead of let
  to match the premises with the knowledge base.  `let*` is still used
  to bind the and-branches of the inference trees together.

## Usage

To run the experiments, enter the following

```bash
metta backward-chainer-xp.metta
```

It should outputs empty results indicating that all tests have passed.