Resolution method solver

Algorithm for demonstrating unsatisfiability of predicate logic formulas

How to Utilize the Algorithm:

1. Begin by entering the language symbols.
2. Input the formulas you wish to demonstrate as unsatisfiable.
3. Click on the "Make transformations" button to convert the formulas into disjunct sets.
4. Then, initiate the resolution process by clicking the "Apply Resolution" button.
5. The algorithm will attempt to construct a step-by-step proof with a step count lower than the specified maximum.

It's important to note that the resolution method is semi-computable. If the provided formulas are indeed satisfiable, the algorithm will be unable to provide a solution, regardless of the maximum step count set.