Q. You can select more than two givens, and Proof
Designer will infer the conjunction of all of them.
Select givens P and Q and give the Conjunction command,
and Proof Designer will infer PQ. You can select more than two givens, and Proof
Designer will infer the conjunction of all of them.
You can also use this command to work backwards from your goal. If you
select a goal of the form P1P2...Pn and give the Conjunction
command, then Proof Designer will say that you now have to prove all of the
statements P1, P2, ...,
Pn, and it will say that once these have been proven,
they can be used to infer the goal. If you already have some of these
statements in your givens list, then you can select them too before giving
the Conjunction command. Proof Designer will then require you to prove
only those statements that are not already in your givens list.
Parentheses in your goal can affect how the Conjunction
command works. For example, if you select a goal of the form PQR and give the Conjunction command, then Proof
Designer will say that you must prove P, Q, and R in
order to complete the proof. But if the goal is P(QR), then
Proof Designer will say that you must prove P and QR. Thus, you may want to add or remove
parentheses in your goal before using the Conjunction command. Too add or
remove parentheses, use the Reexpress command.