Advanced Usage

Advanced Usage

This page assumes you have read the page [Basic Usage]. It contains information on advanced features (unsurprisingly).
See also [Settings].

• Advanced Usage
  • Command Line Options
    • One Argument
      • 2+ Arguments
  • Cut Line
  • Magic Mode
  • Features under Options
    • Zoom
      • Automatic parameter choices
      • Show lines in scope of goal
      • Reverse the order of &I
      • Use ≠ for negated identities
  • New Proof from TeX Code

Command Line Options

When launching the Proof Assistant from the command line, you can specify one or more arguments.

One Argument

If you launch with one argument, that argument must be an NDP or NDU file. The Proof Assistant will launch with that file opened.

2+ Arguments

If you launch with two or more arguments, those arguments must form a sequent in TeX code format. The Proof Assistant will launch with that sequent loaded.

Cut Line

This feature is found under Edit. It allows you to insert a new, unjustified line above the current goal.

Magic Mode

This feature is found under Edit. Running Magic Mode will complete every automatic rule applicable to the current goal and resource (and any created lines), up to 10 rules. Magic Mode will be stopped by any sort of choice or required user input.

Magic Mode is experimental.

Features under Options

Zoom

I hope this is self-explanatory.

Automatic parameter choices

When selected, rules that require new parameters (e.g. existential elimination) will automatically generate them. When deselected, such rules will require the user to input a parameter. If the user inputs an illegal parameter, they will be warned and the relevant justification flagged.

This option is selected by default.

Show lines in scope of goal

When selected, lines not in scope of the current goal will be greyed out.

Reverse the order of &I

Normally, applying &I to (p&q), when neither p nor q is found in scope of the current goal, will generate two new lines - first p and second q. With this option selected, q will be generated first, and p second.

Use ≠ for negated identities

When selected, (a≠b) will be shown, rather than ~(a=b). This option is automatically enabled when changing to Q or PA.

New Proof from TeX Code

This allows you to start a proof from a TeX code format input. To learn how to use this style of input, study the output generated by Export -> To TeX code. This style is the same as that used for command line starts.