Propositional Logic Proofs

Demonstration Rules

Heads you win; tails I lose; tails. |- You win.

Mendelson's Axiomatization

{p = >q, q => r} |- (p => r)

{} |- (p => p)

{p} |- ~~p

Hilbert's Axiomatization

Kleene's Axiomatization

Rosser's Axiomatization

Resolution

Heads you win; tails I lose. |- You win.

Relational Logic Proofs

Demonstration Rules

Various premises |- f(harry,ralph)

Resolution

Herbrand Logic Proofs

Demonstration Rules

Resolution