Enter the first sentence in the input:
Press Enter, and Ruzsa will check if the sentence is syntactically correct:
Once you enter a correct sentence, it will turn into a node of the tree representing the analytic tableau:
Next, you can add further sentences with the Add button:
On smaller desktops and mobile devices, you can find the Add button in the top toolbar:
New sentences are added as leaves to the tree:
If you hover your cursor over (or on touchscreen devices, long tap) a sentence, the breakdown menu will appear:
Select the breakdown rule you want to use, and enter the derived sentences:
When you're ready, click on the Check Step button, and Ruzsa will check if your breakdown step is correct.
If the step is correct, the breakdown's color will change from grey to black, and the broken-down sentence will be marked with strikethrough:
The complete set of breakdown rules is described in detail on the
Method of analytic tableaux Wikipedia page. The first-order
rules of Ruzsa are the ones contained in the
First-order tableau without unification
subsection. Closure is denoted by * derived from
the lower closing node:
You can clear the current tableau and start a new one by clicking on the Ruzsa logo:
