Systém automatického dokazovania pomocou rezolúcie

Operácia	Symboly	Použitie
Konjunkcia (AND)	∧	A and B   A ∧ B (A and B)   (A ∧ B) A and (ψ)   A ∧ (ψ) (φ) and B   (φ) ∧ B (φ) and (ψ)   (φ) ∧ (ψ)
	and
	*
	.
	&
	&&

Operácia	Symboly	Použitie
Negovaná konjunkcia (NAND)	↑	A nand B   A ↑ B (A nand B)   (A ↑ B) A nand (ψ)   A ↑ (ψ) (φ) nand B   (φ) ↑ B (φ) nand (ψ)   (φ) ↑ (ψ)
	nand
	⊼

Operácia	Symboly	Použitie
Negácia	¬	¬A   ¬ A   ¬ (φ)   ¬(φ) not A   not(φ)   not (φ)
	neg
	not
	~
	!
	-

Operácia	Symboly	Použitie
Disjunkcia (OR)	∨	A or B   A ∨ B (A or B)   (A ∨ B) A or (ψ)   A ∨ (ψ) (φ) or B   (φ) ∨ B (φ) or (ψ)   (φ) ∨ (ψ)
	or
	+
	|
	||

Operácia	Symboly	Použitie
Negovaná disjunkcia (NOR)	↓	A nor B   A ↓ B (A nor B)   (A ↓ B) A nor (ψ)   A ↓ (ψ) (φ) nor B   (φ) ↓ B (φ) nor (ψ)   (φ) ↓ (ψ)
	nor
	⊽

Operácia	Symboly	Použitie
Implikácia (IMPLIES)	⇒	A implies B   A ⇒ B (A implies B)   (A ⇒ B) A implies (ψ)   A ⇒ (ψ) (φ) implies B   (φ) ⇒ B (φ) implies (ψ)   (φ) ⇒ (ψ)
	implies
	=>
	>
	→

Operácia	Symboly	Použitie
Vylučovacia disjunkcia (XOR) Negovaná ekvivalencia	xor  ⊕	A xor B   A ⊕ B (A xor B)   (A ⊕ B) A xor (ψ)   A ⊕ (ψ) (φ) xor B   (φ) ⊕ B (φ) xor (ψ)   (φ) ⊕ (ψ)
	eor   nequiv
	exor   neq
	⊻   ↮

Operácia	Symboly	Použitie
Ekvivalencia Negovaná vylučovacia disjunkcia (XNOR)	⇔   ⊙	A eq B   A ⇔ B (A eq B)   (A ⇔ B) A eq (ψ)   A ⇔ (ψ) (φ) eq B   (φ) ⇔ B (φ) eq (ψ)   (φ) ⇔ (ψ)
	equiv   eq
	xnor   iff
	↔   <->
	<>   <=>

Operácia	Symboly	Použitie
Negovaná implikácia (NIMPLIES)	nimplies ⇏	A nimplies B (A nimplies B) A nimplies (ψ) (φ) nimplies B (φ) nimplies (ψ)