ATP using Resolution
Resolution
Syntax
Manual
Truth tables
16px
18px
24px
32px
48px
Font size:
Morning
Noon
Sunset
Midnight
Matrix
Select theme:
Output
Resolution tree
Resolution table
Copy Output
Everything
Formula simplification
Negation steps
Negated formula
CNF conversion steps
CNF formula
Set notation
Copy Tree
Copy Table
Copied
---
Simple input
Symbolic input
LaTeX input
ASCII input
DIMACS input
Examples:
This field is required
SUBMIT
Resolution strategy:
Full
Unit
Linear
Reduced tree
Fully parenthesized formula
