Module 03

Resolution Solver

Enter a propositional formula. The solver converts it to CNF, extracts clauses, and applies the resolution method to determine satisfiability.

Resolution SAT
⊢□
Formula Input
ℹ
Operators: ~ NOT  |  & AND  |  | OR  |  -> IMP  |  <-> IFF
Example: (p -> q) & (~q) & p
Examples:
Insert:
⊢□
Ready to solve
Enter a formula and click Solve to see the full resolution proof
✦ AI Explanation Claude · Streaming