Proofs in equivalence of PC Systems

Propositional Calculus(PC) Logic System can be defined in four different ways: Principia, Hilbert, Lukasiewicz and Rosser.

The following table are the proofs of equivalence between these PC based systems by using SystemOnTPTP.

PCDefns.ax are the definitions of PC systems.
To
From
PCHilbert PCPrincipia PCLukasiewicz PCRosser
PCHilbert X 4 out of 4 proved 3 out of 3 proved 3 out of 3 proved
PCPrincipia 2 out of 12 proved X 0 out of 3 proved 1 out of 3 proved
PCLukasiewicz 7 out of 12 proved 3 out of 4 proved X 0 out of 3 proved
PCRosser 9 out of 12 proved 3 out of 4 proved 2 out of 3 proved X

Succeeded on
Computer : rockville.cs.miami.edu
FreeSwap : 478MB
SpareCPUs : 1
NumberOfCPUs : 1
Model : i686 i686
SwapInUse : 30MB
FreeRAM : 272MB
CPUModel : Intel(R) Pentium(R) 4 CPU 2.00GHz
RAMPerCPU : 503MB
OS : Linux 2.6.9-1.667
CPUSpeed : 1994MHz

-- By Weina Shen

w.shen@umiami.edu