Skip to content
Minimal propositional logic for the Occam proof assistant.
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
Derived rules
Rules
README.md
meta.json
metastatement.bnf
pattern.lex
statement.bnf

README.md

Minimal Propositional Logic

Minimal propositional logic for the Occam proof assistant.

[ \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{[ConjunctionLeftElimination]} ] [ \frac{P\land{Q}}{Q}\quad\small\text{[ConjunctionRightElimination]} ]   [ \frac{P}{P\lor{Q}}\quad\small\text{[DisjunctionLeftIntroduction,LeftAddition]} ] [ \frac{Q}{P\lor{Q}}\quad\small\text{[DisjunctionRightIntroduction,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{[BiconditionalLeftElimination]} ] [ \frac{P\iff{Q}}{Q\Rightarrow{P}}\quad\small\text{[BiconditionalRightElimination]} ]

Resources

Contact

You can’t perform that action at this time.