If you have givens of the forms P∨Q and ¬P, then you may infer Q. More generally, if you have a given of the form P1∨P2∨…∨Pn and you also have the negations of some of the statements P1, P2, …, Pn as givens, then you can infer that one of the other statements in the list must be true. Select all of the givens involved in the inference and give the Disjunctive Syllogism command, and Proof Designer will make the inference.
You can also use this command to work backwards from your goal. If you have a given of the form P1∨P2∨…∨Pn and your goal is the disjunction of some of the statements P1, P2, …, Pn, then you could complete the proof by first proving the negations of the other statements in the list and then using the disjunctive syllogism rule. Select the given P1∨P2∨…∨Pn and the goal and give the Disjunctive Syllogism command. Proof Designer will say that you now have to prove the negations of those statements in the list P1, P2, …, Pn that don't appear in the goal, and it will say that once these have been proven, they can be used, together with the statement P1∨P2∨…∨Pn, to infer the goal. If you already have some of these negations in your givens list, then you can select them too before giving the Disjunctive Syllogism command. Proof Designer will then require you to prove only those negations that are not already in your givens list.
Parentheses in your given can affect how the Disjunctive Syllogism command works. For example, suppose you have a given of the form P∨Q∨R and your goal is P. If you select this given and goal and give the Disjunctive Syllogism command, then Proof Designer will say that you must prove both ¬Q and ¬R in order to complete the proof. But if the given is P∨(Q∨R), then Proof Designer will say that you must prove ¬(Q∨R). Thus, you may want to add or remove parentheses in your given before using the Disjunctive Syllogism command. Too add or remove parentheses, use the Reexpress command.