Natural Commands

PhoX's natural commands are conceived as an intermediate language for a forthcoming natural language interface. But, they are also directly usable with the following advantages and disadvantages compared with the usual tactics:

advantages

Proof are readable and more robust (when you modify something in your theorems, less work is necessary to adapt your proofs).

disadvantages

The automatic reasoning of PhoX is pushed to the limit and in the current implementation it may be hard to do complex proofs with natural commands. You can greatly help the system by using the rmh or slh commands to select the hypotheses.

Remark: some of the feature described here are signaled as not yet implemented.

• Examples
• The syntax of the command
• Semantics