Phobos: Proof Help

There are four levels of proof available.

(1) The definite level.

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

+d x

(2) The plausible with ambiguity propagation (likely) level.

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

+l x

(3) The plausible level without ambiguity propagation.

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

+p x

(4) The supported level.

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

+s 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 +l x cannot be proved, type

-l x

To prove that +p x cannot be proved, type

-p x

To prove that +s x cannot be proved, type

-s x

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

Let a be one of d, l, p, s.

If +a x then not -a x.

If -a x then not +a x.

The levels of proof are related as follows.

If +d x then +l x.

If +l x then +p x.

If +p x then +s x.

If -s x then -p x.

If -d x then -l x.

If -l x then -d x.