Priority of operators:
- NOT (¬)
- NAND (↑)
- NOR (↓)
- NIMPLIES (⇏)
- XOR (⊕)
- AND (∧)
- OR (∨)
- IMPLIES (⇒)
- EQUIV (⇔)
Input and Output
There is an option on the left side to change the size of text in input and output field.
On the right side, there is an option to change the appearance of the website.
To evaluate the formula, enter the formula in the input field using the keys below the field, or simply copy the formula from LaTeX into the field. It is also possible to enter formulas manually, all possible accepted forms of operators are listed in the "Syntax" section. The input field checks the syntax.
After pressing the "SUBMIT" button, the output window will appear and the following data will be written in the left part of the output window:
- Input formula: the formula read from the input field.
- Simplified formula: if the formula contains excess parentheses or multiple negations, they will be removed from it.
- Negation of the formula: How to negate a given formula. Operators that are negated in a given step are highlighted in red.
- Negated formula: The result of the negation of the formula
Subsequently, the formula will be converted into Conjunctive Normal Form (CNF). This is done using the following steps:
- Removal of implication and equivalence: highlighted implications/equivalences are rewritten as follows in the next step:
φ ⇔ ψ ≡ (φ ⇒ ψ) ∧ (ψ ⇒ φ) ≡ (¬φ ∨ ψ) ∧ (¬ψ ∨ φ)
φ ⇒ ψ ≡ ¬φ ∨ ψ
- Putting the negation in parentheses and removing the operators ↑, ↓, ⇏, ⊕:
¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ
¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ
φ ↑ ψ ≡ ¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ
φ ↓ ψ ≡ ¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ
φ ⇏ ψ ≡ ¬(φ ⇒ ψ) ≡ ¬(¬φ ∨ ψ) ≡ φ ∧ ¬ψ
φ ⊕ ψ ≡ ¬(φ ⇔ ψ) ≡ ¬((¬φ ∨ ψ) ∧ (¬ψ ∨ φ)) ≡ φ ∧ ¬ψ ∨ ψ ∧ ¬φ
- Inserting disjunctions inside parentheses:
φ ∨ (ψ ∧ θ) ≡ (φ ∨ ψ) ∧ (φ ∨ θ)
(ψ ∧ θ) ∨ φ ≡ (ψ ∨ φ) ∧ (θ ∨ φ)
(φ ∧ ψ) ∨ (θ ∧ ω) ≡ (φ ∨ θ) ∧ (φ ∨ ω) ∧ (ψ ∨ θ) ∧ (ψ ∨ ω)
- Simplification by removing clauses with complementary literals, duplicate clauses and duplicate literals:
¬φ ∨ φ ≡ ⊤
(φ ∨ ψ) ∧ (ψ ∨ φ) ≡ φ ∨ ψ
φ ∨ ψ ∨ φ ≡ φ ∨ ψ
If any of these steps did not cause any change in the formula, it will not be written in the output window.
- Negated CNF: Result of transfer to CNF
- Set notation: conversion of CNF to set notation
- The result of the resolution is written at the end of the window, i.e. whether the given formula is a tautology or not.
Under the input field, it is possible to set the resolution strategy and the method of listing the tree.
Resolution strategies:
- Full - the program will try to combine each clause with each other to achieve a resolution result. However, it prioritizes unit clauses first.
- Unit - the program must use at least one unit clause for each resolution.
- Linear - the program always uses the resolvent of the previous step in the next step.
Reduced Tree - Instead of showing all clauses and resolvers in the tree, it will show only those that led to the result.
In the right part of the output window it is possible to switch between 2 representations of resolution, namely:
- Resolution table: This table lists all clauses and resolvents in set notation in the second column. The table shows the resolution procedure used to determine whether a given formula is a tautology. Clauses and resolvents are numbered in the first column of the table. The third column of the table shows which clauses were used to create a given resolvent using resolution.
- Resolution tree: Based on the selected strategy of resolution, the tree will contain steps leading to the result of the resolution.
Every part of output, namely the text output, the table, and the tree can be copied using the buttons under the output window in a form of LaTeX code. The table is converted to tabular format and tree is converted to an image in tikz format.
