This is a tool created for students taking the Logic and Logic Programming module at the University of Kent. The tool can be used to work through solutions to semantic equivalence problems. You apply rules to a formula by highlighting the section you wish to change(the symbols and variables), selecting the rule and pressing the Apply Rule button. If the rule can be applied, the changed formula will appear on a new line in the table.
The tool may remove unnecessary brackets, so it is important to understand the rules of precedence when using it. Have a look at the rules of precedence section on the Rules page for an explanation.
In the Settings section of the navigation bar, you can choose whether the rules are displayed while you are working on an exercise. The rules' names appear at the side of the page and can be clicked to show a pop-up of the rule. You can also choose to work on exercises both forwards and backwards. When working backwards, you can apply rules to the formula which you are trying to reach. There is also a previous step button, when clicked you select a line of your workings to return to. Be careful when using this feature, as you will lose all the workings which follow the line you choose.
The Semantic Equivalence rules can be seen in the Rules section, you can click on a rule to see an example of it being applied. In the Exercises section, there are exercises taken from the module classes. You can click on any and you will be taken to the tool page with the formulae already entered.