- You may use uppercase and lowercase roman letters for propositional variables. You may also use strings of length ≥ 2, and they should start with [A,..,B,a,..,z] and be followed by [A,..,Z,a,..,z,0,..,9,_].
- In order to input connectives, you may click the symbols in the virtual keyboard shown at the top of the screen with mouse, or hit the corresponding key shown right below the symbol.
- The truth functions for the connectives are shown below.
- If you enter more than one formulas separated by semicolons(;), the truth tables for all formulas are constructed simultaneously. For instance, if you enter a∨b ; ￢a→b ; ￢b→a and click [Go], then you can easily check that all these formulas have the same truth function, and hence equivalent.
- You may hit [Enter] instead of clicking [Go].
- The priority of the connectives are: ￢ is highest, then ∧, ∨, ↕, ↑, ↓ are of the same intermeiate priority, and finally →, ↔ are of the same lowest priority. You can remove unnecessary parentheses using these priorities. For instance (a∧(￢b))→((￢c)↕d) may be written as a∧￢b→￢c↕d.
- Using the fact that ∧ and ∨ satisfy the associative law, you can remove parentheses: e.g., you may write ((a∧b)∧c)→((a∨b)∨(c∨d)) as a∧b∧c→a∨b∨c∨d. Internally, a∧b∧c are handled as if it has a single connective with arity 3. In the truth table, the truth values of such a formula are given below the leftmost ∧ . See below:
- Using the menus [Open], [Save] and [Save as...], you may save and retrieve formulas. Note that the formula you saved is not securely stored because the storage space is shared with other people.
- For the preparation of lecture note and/or slides, [TeX export] can be useful. The source needs proormood_en.sys, which you can download by clicking the link. You can close the TeX export area by clicking [TeX export] again. A sample LaTeX source is given below.
\documentclass{article} \usepackage{proofmood} \begin{document} \begin{truthtable}{|>{\tt}c|>{\tt}c||>{\tt}c|>{\tt}c|>{\tt}c|}\hline \makebox[1.7em]{\tsf{A}} & \makebox[1.7em]{\tsf{B}} & \tsf{A} & $\limpl$ & \tsf{B}\ttnl \hline 1 & 1 & 1 & 1 & 1\ttnl \hline 1 & 0 & 1 & 0 & 0\ttnl \hline 0 & 1 & 0 & 1 & 1\ttnl \hline 0 & 0 & 0 & 1 & 0\ttnl \hline \multicolumn{2}{|c||}{\pmfont{Stage}} & 1 & \bf 2 & 1\ttnl \hline \ttw & \ttw & \ttw & \ttw & \ttw \\ \end{truthtable} \end{document} - Matching parentheses can be highlighted. This function is enabled by Shift-Alt. (Default mode is 'disabled'.) With this function enabled, matching parentheses are highlighted when the caret is put immediately left to the parenthesis(left or right). This functionality may not be greatly valuable in Truth Table but will be surely useful in 1st-order Fitch proof system.