Infer Menu:

Addition Command

From a given statement P you can infer P∨Q, for any statement Q. Select any given P and give the Addition command, and a dialog box will open asking you to fill in the blank in the statement P∨____ in order to specify what inference you want to make.

You can also use this command to work backwards from your goal. If you select a given P and goal P∨Q and give the Addition command, Proof Designer will infer the goal from the given.

Parentheses in your goal can affect how the Addition command works. For example, if you select a given P and goal P∨Q∨R and give the Addition command, then Proof Designer will infer the goal from the given. But if the goal is (P∨Q)∨R, then the command won't work. Thus, you may want to add or remove parentheses in your goal before using the Addition command. Too add or remove parentheses, use the Reexpress command.