These are the menu options for the main proof windows. Each one can be assigned a key command.
Start a new proof. A new window is opened for this proof.
Open an existing proof in a new window.
Save the current proof.
Save the current proof under a different name.
Export the current proof to a LaTeX file.
Close the current proof.
Exit Aris. But since logic is so much fun, I doubt you’ll ever want to use this one.
Insert a new premise at the end of the other premises.
Insert a new conclusion after the current line if it is a conclusion, or at the start of the conclusions if it is a premise.
Begin a new subproof after the current line if it is a conclusion, or at the start of the conclusions if it is a premise. This is unavailable in boolean mode, since subproofs can’t be used.
End the current subproof, if there is one. Otherwise, this doesn’t do anything. This is unavailable in boolean mode, since subproofs can’t be used.
Undo the last modification to the current proof. On a new file, this does nothing.
Undo an undo operation. If no undo has been made, then this does nothing.
Copy the current line.
Kill, or cut, the current line. This removes the line from the proof.
Insert the copied/killed line.
Evaluate the logical validity of the current line.
Evaluate the logical validity of the current proof. This evaluates each line of the proof.
Toggle the goal window for the current proof.
Toggle boolean mode for the current proof See Boolean Rules.
Import another proof into this one. This will merge the premises of the other proof into the current one, and insert the goals of the other proof as conclusions. In addition, it sets the conclusions’ references as the premises, and sets them all to use the lemma rule see lm.
Toggle the rules window.
Change the font size to small (8pt).
Change the font size to medium (12pt).
Change the font size to large (16pt).
Change the font size to a custom size. This menu option opens a dialog box with a numerical entry.
Display Aris help. This is the only key command that cannot be modified.
Displays information about GNU Aris.