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.
Best Answer
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