# Is it possible to draw resolution proof tree in beamer

How to draw a resolution tree such as the example here

-
Asking a question like this is not likely to get many answers. There are plenty of tikz-qtree questions and answers on the site, and the tikz-qtree documentation has an example of how to draw a tree upside down. If you show us a working document with what you're having trouble with, perhaps people can help you. – Alan Munn Apr 10 '13 at 13:05
No need to down vote below -1, especially to a new member – cmhughes Apr 10 '13 at 15:20
Hi math :) and welcome to TeX.sx. In its current form, your question might not receive many answers. Please take a look at the How to Ask-page and try to improve your question according to the guidance found there. if possible please add a minimal working example (MWE). If you have questions about what to do or if you don't quite understand what this means, please ask for clarification using the add comment function. – texenthusiast Apr 10 '13 at 15:41
Many thanks, guys. That tree can be written in latex? – math Apr 10 '13 at 17:00

The tree can be easily done using TikZ:

\documentclass{article}
\usepackage{tikz}
\usetikzlibrary{calc,fit,trees}

\begin{document}

\begin{tikzpicture}[
grow'=up,
level 1/.style={sibling distance=14em},
level 2/.style={sibling distance=6em}]
\node (f) {False}
child { node (1l) {$p(a)$}
child {node (2ll) {$\neg p(a)$}}
child {node (2lr) {$p(a)\vee p(b)$}}
}
child {node (1r) {$\neg p(a)$}
child {node (2rl) {$p(X)\vee r(X)$}}
child {node (2rr) {$\neg r(b)$}}
};
\end{tikzpicture}

\end{document}


The only thing that might not be trivial is to draw the closed paths surrounding some groups of formulas; one possible approach here would be to use Jake's answer to padded boundary of convex hull:

\documentclass{article}
\usepackage{tikz}
\usetikzlibrary{calc,fit,trees}

\newcommand{\convexpath}[2]{
[
create hullnodes/.code={
\global\edef\namelist{#1}
\foreach [count=\counter] \nodename in \namelist {
\global\edef\numberofnodes{\counter}
\node at (\nodename) [draw=none,name=hullnode\counter] {};
}
\node at (hullnode\numberofnodes) [name=hullnode0,draw=none] {};
\pgfmathtruncatemacro\lastnumber{\numberofnodes+1}
\node at (hullnode1) [name=hullnode\lastnumber,draw=none] {};
},
create hullnodes
]
($(hullnode1)!#2!-90:(hullnode0)$)
\foreach [
evaluate=\currentnode as \previousnode using \currentnode-1,
evaluate=\currentnode as \nextnode using \currentnode+1
] \currentnode in {1,...,\numberofnodes} {
-- ($(hullnode\currentnode)!#2!-90:(hullnode\previousnode)$)
let \p1 = ($(hullnode\currentnode)!#2!-90:(hullnode\previousnode) - (hullnode\currentnode)$),
\n1 = {atan2(\x1,\y1)},
\p2 = ($(hullnode\currentnode)!#2!90:(hullnode\nextnode) - (hullnode\currentnode)$),
\n2 = {atan2(\x2,\y2)},
\n{delta} = {-Mod(\n1-\n2,360)}
in
{arc [start angle=\n1, delta angle=\n{delta}, radius=#2]}
}
-- cycle
}

\begin{document}

\begin{tikzpicture}[
grow'=up,
level 1/.style={sibling distance=14em},
level 2/.style={sibling distance=6em}]
\node (f) {False}
child { node (1l) {$p(a)$}
child {node (2ll) {$\neg p(a)$}}
child {node (2lr) {$p(a)\vee p(b)$}}
}
child {node (1r) {$\neg p(a)$}
child {node (2rl) {$p(X)\vee r(X)$}}
child {node (2rr) {$\neg r(b)$}}
};
\draw[cyan!70!black] \convexpath{f,1l.west,1r.east}{13pt};
\draw[red!70!black] \convexpath{1r,2rl.west,2rr.east}{12pt};
\end{tikzpicture}

\end{document}


You have access to many resources related to TikZ:

-