A matrix model for combinational circuits is used as a framework for redundancy detection and elimination. The detection procedure 'tracks' the logic changes encountered between fan-out nodes (the source of all redundancy) and primary outputs, and highlights those paths which indicate redundancy in other paths fanning out from the same fan-out node. The matrix model is then used to remove such redundancies, and so derive an equivalent irredundant form of the original circuit.