/theorem-prover

A small propositional calculus theorem prover. Mainly made to enhance my own understanding of formal verification and proof procedure.

Primary LanguageJavaScriptMIT LicenseMIT

Theorem Prover

A small propositional logic theorem prover. Mainly made to enhance my own understanding of formal verification and proof procedure.

What is propositional logic?

Propositional Logic is a branch of logic that restricts itself to truths values (also called sentences) and logical connectives such as "AND", "OR", and "If ..., THEN ...".

The truth values are given a letter such as "P" and the connectives are given symbols such as "->", "^", and "<->" (these are simply ascii representations of the symbols.

These can then be constructed in formulas such as "P->P", which is read in English as "If P is true, Then P is true" (If you make P a sentence such as "The sky is blue" then the formula woould read "If the sky is blue, then the sky is blue.")

This is an example of a tautology (something that is always true), and we can prove that with some formal system for proving theorems in propositional logic.