Minimal propositional logic for Occam.
[ \frac{[P];...;Q}{P\Rightarrow{Q}}\quad\small\text{[ImplicationIntroduction,ConditionalProof]} ]
[ \frac{P\Rightarrow{Q};;P}{Q}\quad\small\text{[ModusPonens,ImplicationElimination,RuleOfDetachment]} ]
[ \frac{P\Rightarrow{Q};;P\Rightarrow\neg{Q}}{\neg{P}}\quad\small\text{[NegationIntroduction,ProofByNegation]} ]
[ \frac{P;;Q}{P\land{Q}}\quad\small\text{[ConjunctionIntroduction]} ]
[ \frac{P\land{Q}}{P}\quad\small\text{[ConjunctionRightElimination]} ]
[ \frac{P\land{Q}}{Q}\quad\small\text{[ConjunctionLeftElimination]} ]
[ \frac{P}{P\lor{Q}}\quad\small\text{[DisjunctionRightIntroduction,LeftAddition]} ]
[ \frac{Q}{P\lor{Q}}\quad\small\text{[DisjunctionLeftIntroduction,RightAddition]} ]
[ \frac{P\Rightarrow{R};;Q\Rightarrow{R};;P\lor{Q}}{R}\quad\small\text{[DisjunctionElimination,ProofByCases]} ]
[ \frac{P\Rightarrow{Q};;Q\Rightarrow{P}}{P\iff{Q}}\quad\small\text{[BiconditionalIntroduction]} ]
[ \frac{P\iff{Q}}{P\Rightarrow{Q}}\quad\small\text{[BiconditionalRightElimination]} ]
[ \frac{P\iff{Q}}{Q\Rightarrow{P}}\quad\small\text{[BiconditionalLeftElimination]} ]
As well as these rules there are many derived rules. See the package contents for details.