Summary: We propose a general framework for first-order functional logic programming, supporting lazy functions, non-determinism and polymorphic datatypes whose data constructors obey a set \({\mathcal C}\) of equational axioms. On top of a given \({\mathcal C}\), we specify a program as a set \({\mathcal R}\) of \({\mathcal C}\)-based conditional rewriting rules for defined functions. We argue that equational logic does not supply the proper semantics for such programs. Therefore, we present an alternative logic which includes \({\mathcal C}\)-based rewriting calculi and a notion of model. We get soundness and completeness for \({\mathcal C}\)-based rewriting w.r.t. models, existence of free models for all programs, and type preservation results. As operational semantics, we develop a sound and complete procedure for goal solving, which is based on the combination of lazy narrowing with unification modulo \({\mathcal C}\). Our framework is quite expressive for many purposes, such as solving action and change problems, or realizing the GAMMA computation model.