Transformational Proof

Definition

A transformational proof () is a means of determining that two well-formed formulas of propositional logic, and , are logically equivalent repeated exchange of sub-formulas that turn into using logical laws.

Logical laws are listed in depth in Logical Operators.

This is the same idea as a direct proof, but with formal proofs, we seek to create unambiguous proofs that can be mechanically verified with a computer program.

Property

Transformational proofs for propositional logic are both sound and complete

Non-exhaustive list of laws

These may seem obvious, but remember, we're trying to give a more "formal" definition of a transformation proof.

  • comm_assoc
  • lem
  • contr
  • impl
  • idemp
  • neg
  • simp1
  • dm (De Morgan's law)
  • distr
  • contrapos
  • equiv
Example

Prove:

proof

Two implicit rules: