How to automatically create proofs in Boolean Algebra Given a complete set of axioms (for example, associativity, communtative, distributivity, identity, annihilator, idepotence, and the "complementation" laws) for boolean algebra, I know any other true statement follows logically from these axioms. As an example, Boolean algebra question. shows someone asking how to prove a statement using the laws of boolean algebra.
II've been trying to find a constructive method of generating such a proof (just for boolean algebra, I know this isn't possible in general), but can't seem to find one published anywhere.
By just using breadth-first search I could construct a proof (in a possibly huge amount of time) for any true theorem, but such a system would never terminate for any false theorem.
 A: To prove a statement in Boolean algebra like $\phi(A_1,A_2,\dots,A_n)=\psi(A_1,A_2,\dots,A_n)$ you can put both $\phi$ and $\psi$ into some normal form, e.g. CNF or DNF, which can be done algorithmically (see the linked wikipedia articles). These normal forms are essentially unique (up to reordering of terms e.g. $A \wedge B=B \wedge A$), so $\phi=\psi$ iff they have the same normal form.
A: You can systematically put both statements into their Canonical Conjunctive (or Disjunctive) Normal Form (cCNF or cDNF) relative to the shared aet of variables.
For example, if one statement is $(A \lor B) \land (A \lor \neg B)$ and the other is $(A \land C) \lor (A \land \neg C)$, then their shared set if variables is $\{ A, B,C \}$, and for both statements their cDNF with regard to set of variables is $(A \land B \land C) \lor (A \land B \land \neg C) \lor (A \land \neg B \land C) \lor (A \land \neg B \land \neg C)$
The algorithm to put any propositional logic statement into its cDNF with regard to some set of variables is fairly easy: 


*

*Rewrite all operators into $\neg$, $\lor$, and $\land$'s

*Keep applying DeMorgan and Double Negation until any negations left are negations of atomic variables (the statement is now in NNF)

*Keep applying Distribution of $\land$ over $\lor$ until there are no such Distributions to be done (the statement is now in DNF)

*Simplify as much as possible using Annihilation, Identity, Complement, and Idempotence

*Use Adjacency to make sure every term includes references to each variable from the shared variable set (e.g. $A$ becomes $(A \land B) \lor (A \land \neg B)$

*Use commutation to get all terms in the order as specified by the cDNF
