Okay, I'm trying to prove the constructive dilemma:
\{p\lor q, p\to r, q\to r\} \vdash r
And I was attempting a proof tree for it in ebproofs and it is giving me some problems.
My code looks like this:
\begin{prooftree}
\Hypo{\neg r} \Hypo{p\to r} \Infer{2}[MT]{\neg p}
\Hypo{p\lor q} \Infer{2}[MT]{q}
\end{prooftree}
Up to this point it turns out fine. But when I add this:
\begin{prooftree}
\Hypo{\neg r} \Hypo{p\to r} \Infer{2}[MT]{\neg p}
\Hypo{p\lor q} \Infer{2}[MT]{q}
\Hypo{\neg r} \Hypo{p\to q} \Infer{2}[MT]{\neg q}
\end{prooftree}
I know this is an unfinished proof, but I get a problem here when I try to run the code. Apparently it's a "malformed proof tree".
MT = modus tollens here.