有没有办法在Jupyter Notebook中绘制bussproof风格的树形图？

huangapple
go评论75阅读模式
英文:

Is there a way to draw bussproof style tree diagram in Jupyter Notebook?

问题

以下是您要翻译的内容：

一个示例的bussproof样式树状图如下所示。

有没有办法在Jupyter Notebook中绘制bussproof风格的树形图？

上图显示了命题公式$\neg A \to (B \vee C)$的抽象语法树（AST）。可以使用LaTeX包bussproof.sty来绘制这样的图。

我知道我可以使用graphviz来绘制AST，但我不知何故更喜欢简单的bussproof样式图。所以我的问题是：是否有一种方法可以在Jupyter Notebook中为逻辑公式和/或自然演绎证明绘制bussproof样式的树状图？

我尝试过graphviz、treelib和plotly。这些都不令人满意。我想要的是bussproof样式的图。

英文:

An example of bussproof style tree diagram is shown below.

有没有办法在Jupyter Notebook中绘制bussproof风格的树形图？

Above diagram shows the AST(abstract syntax tree) of the propositional formula $\neg A \to (B \vee C)$. Such a diagram can be drawn using the LaTeX package bussproof.sty.

I am aware that I could use graphviz for drawing AST, but somehow I prefer the simple bussproof style diagram. So here is my question: is there a way to draw bussproof style tree diagram for logical formulas and/or Natural deduction proof in Jupyter Notebook?

I tried graphviz, treelib, and plotly. None of these were satisfactory. I want bussproof style diagram.

答案1

得分: 1

以下是您要翻译的内容：

"不是Jupyter Notebook用户，但相当肯定您可以使用Graphviz完成您想要的大部分或全部操作。下面有两个示例，一个是您的原始示例，另一个来自“bussproofs.sty用户指南”。我不是逻辑学家，但自动化单个单元格看起来相当可行。根据输入，自动化整个过程可能不会太糟糕。每个AST都被创建为单个“类似HTML的”节点标签（https://graphviz.org/doc/info/shapes.html#html）。一些字符不正确，但这应该很容易修复。"

请注意，我已经将文本内容翻译为中文。

英文:

Not a Jupyter Notebook user, but pretty sure you can do most or all of what you want with Graphviz.
Below are two examples, your original & one from "bussproofs.sty
A User Guide".
I'm not a logician, but automating individual cells looks pretty doable. Depending on the input, automating the whole thing might not be too bad.
Each AST is created as a single "html-like" node label (https://graphviz.org/doc/info/shapes.html#html).
Some of the characters are incorrect, but that should be easy to fix.

graph B {
  rankdir=LR    // just for demo purposes

  { rank=same   // just for demo purposes  
  t1 [shape=plaintext,label=<
  <TABLE CELLSPACING="0" CELLPADDING="2" BORDER="0">
  <TR>
    <TD BORDER="1" sides="b">A</TD>
    <TD> </TD>
    <TD BORDER="1" sides="b">B</TD>
    <TD BORDER="1" sides="b"> </TD>
    <TD BORDER="1" sides="b">C</TD></TR>
  <TR>
    <TD BORDER="1" sides="b">¬</TD>
    <TD BORDER="1" sides="b"> </TD>
    <TD BORDER="1" sides="b"> </TD>
    <TD BORDER="1" sides="b">∨</TD>
    <TD BORDER="0"> </TD>
  </TR>
  <TR>
    <TD > </TD>
    <TD>→</TD>
    <TD > </TD>
    <TD > </TD>
    <TD > </TD>
  </TR>  
  </TABLE>>]

  t2 [shape=plaintext,label=<
  <TABLE CELLSPACING="0" CELLPADDING="2" BORDER="0">
  <TR>
    <TD BORDER="0" > </TD>
    <TD BORDER="0" > </TD>
    <TD BORDER="0" > </TD>    
    <TD BORDER="1" sides="b">⌊A⌋</TD>
    <TD BORDER="0"> </TD>
  </TR>

  <TR>
    <TD BORDER="0" > </TD>
    <TD BORDER="0" > </TD>
    <TD BORDER="0" > </TD>    
    <TD BORDER="0" >Π<sub>2</sub></TD>
    <TD BORDER="0"> </TD>
  </TR>  
  <TR>
    <TD BORDER="0" >Π<sub>1</sub></TD>
    <TD BORDER="0" > </TD>
    <TD BORDER="0" > </TD>
    <TD BORDER="1" sides="b">B</TD>
    <TD BORDER="0"> </TD>
  </TR>
    <TR>
    <TD BORDER="1" sides="b">A</TD>
    <TD BORDER="1" sides="b"> </TD>
    <TD BORDER="1" sides="b">A</TD>
    <TD BORDER="1" sides="b">→</TD>
    <TD BORDER="1" sides="b">B</TD>    
  </TR>
  <TR>
    <TD > </TD>
    <TD> </TD>
    <TD >B</TD>
    <TD > </TD>
    <TD > </TD>
  </TR>  
  </TABLE>
  >]
  }
  t1--t2  [style=invis]
}

Giving:
有没有办法在Jupyter Notebook中绘制bussproof风格的树形图？

p.s. I like the keypunch - similar to IBM 026

答案2

得分: 0

我已创建了一个Python脚本，用于生成巴斯普鲁夫风格的树形图表。此脚本与Jupyter Notebook兼容，并且也可以在Google Colab平台上使用。您可以在这里访问该脚本。

该脚本还生成可以与bussproofs.sty一起使用的LaTeX源代码。

它包括了命题逻辑的解析器。因此，以下代码生成(1) LaTeX源代码和(2) 树形图表。

input_formula = "not A imp B imp not C and D"
testParser(input_formula, 'bussproof')
testParser(input_formula, 'tree')

生成以下LaTeX源代码：

\begin{prooftree}
\AxiomC{$A$}
\UnaryInfC{$\neg$}
\AxiomC{$B$}
\AxiomC{$C$}
\UnaryInfC{$\neg$}
\AxiomC{$D$}
\BinaryInfC{$\wedge$}
\BinaryInfC{$\rightarrow$}
\BinaryInfC{$\rightarrow$}
\end{prooftree}

和以下图表。

有没有办法在Jupyter Notebook中绘制bussproof风格的树形图？


<details>
<summary>英文:</summary>

I have created a Python script that generates busproof-style tree diagrams. This script is compatible with Jupyter Notebook and can also be used on the Google Colab platform. You can access the script [here](https://colab.research.google.com/drive/1ZlanSUrOCbLW0mJgMsUDdV8bF4B0Ab66?usp=sharing). 

The script also generates LaTeX source that can be used with `bussproofs.sty`.

It includes parser for propositional logic. So the following code generates (1) the LaTeX source and (2) the tree diagram.

input_formula = "not A imp B imp not C and D"
testParser(input_formula, 'bussproof')
testParser(input_formula, 'tree')

Generates the following LaTeX source

\begin{prooftree}
\AxiomC{$A$}
\UnaryInfC{$\neg$}
\AxiomC{$B$}
\AxiomC{$C$}
\UnaryInfC{$\neg$}
\AxiomC{$D$}
\BinaryInfC{$\wedge$}
\BinaryInfC{$\rightarrow$}
\BinaryInfC{$\rightarrow$}
\end{prooftree}

and the following diagram.

[![enter image description here][1]][1]


  [1]: https://i.stack.imgur.com/kIAlw.png

</details>

huangapple
  • 本文由 发表于 2023年5月17日 17:20:26
  • 转载请务必保留本文链接：https://go.coder-hub.com/76270483.html
  • abstract-syntax-tree
  • jupyter-notebook
  • python
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定