Reasoning over networks by symbolic methods

Effective quantifier elimination procedures for the reals allow to solve pr oblems that can be encoded into corresponding first-order formulas includin g ordering constraints. In contrast to constraint logic programming, which is often used in similar areas, this encoding is straightforward, A quantif ier elimination procedure using test point ideas is part of the package RED LOG by the author ct al. REDLOG is part of REDUCE 3.7. We discuss how this method can be used for analysis, sizing, and error diagnosis of physical ne tworks. The focus is on electrical networks.