logo
English Slovak

ATP using Resolution

NOT
A ¬A
1 0
0 1
AND
A B A ∧ B
1 1 1
1 0 0
0 1 0
0 0 0
OR
A B A ∨ B
1 1 1
1 0 1
0 1 1
0 0 0
IMPLIES
A B A ⇒ B
1 1 1
1 0 0
0 1 1
0 0 1
EQUIV / XNOR
A B A ⇔ B
1 1 1
1 0 0
0 1 0
0 0 1
XOR
A B A ⊕ B
1 1 0
1 0 1
0 1 1
0 0 0
NAND
A B A ↑ B
1 1 0
1 0 1
0 1 1
0 0 1
NOR
A B A ↓ B
1 1 1
1 0 0
0 1 0
0 0 0