# Deimos: Proof Help

## Defeasible Logic

There are two levels of proof available.

(1) The definite level.

This level only uses facts and rules with `->` in them. To prove `x` at this level, type

`+D x`

(2) The defeasible level.

This level uses all the facts, rules and the priority (`>`) information. To prove x at this level type

`+d x`

This system can also prove that formulas cannot be proved.

To prove that `+D x` cannot be proved, type

`-D x`

To prove that `+d x` cannot be proved, type

`-d x`

The positive (`+`) and negative (`-`) kinds of proof are related as follows.

Let `P` be `D` or `d`.

If `+P x` then not `-P x`.

If `-P x` then not `+P x`.

The levels of proof are related as follows.

If `+D x` then `+d x`.

If `-d x` then `-D x`.

## Defeasible Logic Variants

The `dt` level of proof does not feature team defeat, but is otherwise the same as the `d` defeasible level of proof.

The `da` level of proof features ambiguity propogation, making it a slightly stronger level of proof than the `d` defeasible level of proof. It is defined in terms of a weaker level, `S`, support. 