Use with JupyterLab/Jupyer Notebook

Mathesis works well with JupyterLab and Jupyter notebooks. This is an example of a notebook that uses Mathesis.

In [1]:

from IPython.display import display, Math

from IPython.display import display, Math

In [2]:

from mathesis.deduction.sequent_calculus import SequentTree, rules
from mathesis.grammars import BasicGrammar

grammar = BasicGrammar()
premises = grammar.parse(["¬A", "A∨B"])
conclusions = grammar.parse(["B"])

from mathesis.deduction.sequent_calculus import SequentTree, rules from mathesis.grammars import BasicGrammar grammar = BasicGrammar() premises = grammar.parse(["¬A", "A∨B"]) conclusions = grammar.parse(["B"])

In [3]:

st = SequentTree(premises, conclusions)

Math(st[1].sequent.latex())

st = SequentTree(premises, conclusions) Math(st[1].sequent.latex())

Out[3]:

$\displaystyle \neg A, A \lor B \Rightarrow B$

In [4]:

st.apply(st[1], rules.Negation.Left())
print(st.tree())

st.apply(st[1], rules.Negation.Left()) print(st.tree())

¬A 1, A∨B 2 ⇒ B 3 [¬L]
└── A∨B 5 ⇒ A 4, B 6

In [5]:

st.apply(st[5], rules.Disjunction.Left())
print(st.tree())

st.apply(st[5], rules.Disjunction.Left()) print(st.tree())

¬A 1, A∨B 2 ⇒ B 3 [¬L]
└── A∨B 5 ⇒ A 4, B 6 [∨L]
    ├── A 7 ⇒ A 8, B 9
    └── B 10 ⇒ A 11, B 12

In [6]:

st.apply(st[9], rules.Weakening.Right())
print(st.tree())

st.apply(st[9], rules.Weakening.Right()) print(st.tree())

¬A 1, A∨B 2 ⇒ B 3 [¬L]
└── A∨B 5 ⇒ A 4, B 6 [∨L]
    ├── A 7 ⇒ A 8, B 9 [wR]
    │   └── A 13 ⇒ A 14
    └── B 10 ⇒ A 11, B 12

In [7]:

st.apply(st[11], rules.Weakening.Right())
print(st.tree())

st.apply(st[11], rules.Weakening.Right()) print(st.tree())

¬A 1, A∨B 2 ⇒ B 3 [¬L]
└── A∨B 5 ⇒ A 4, B 6 [∨L]
    ├── A 7 ⇒ A 8, B 9 [wR]
    │   └── A 13 ⇒ A 14
    └── B 10 ⇒ A 11, B 12 [wR]
        └── B 15 ⇒ B 16

In [8]:

print(st.latex())

print(st.latex())

\begin{prooftree}
\AxiomC{$A \Rightarrow A$}
\RightLabel{$wR}
\UnaryInfC{$A \Rightarrow A, B$}
\AxiomC{$B \Rightarrow B$}
\RightLabel{$wR}
\UnaryInfC{$B \Rightarrow A, B$}
\RightLabel{$\lor$L}
\BinaryInfC{$A \lor B \Rightarrow A, B$}
\RightLabel{$\neg$L}
\UnaryInfC{$\neg A, A \lor B \Rightarrow B$}
\end{prooftree}