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 [Cscr ] of equational axioms. On top of a given [Cscr ], we specify a program as a set [Rscr ] of [Cscr ]-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 [Cscr ]-based rewriting calculi and a notion of model. We get soundness and completeness for [Cscr ]-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 [Cscr ]. Our framework is quite expressive for many purposes, such as solving action and change problems, or realizing the GAMMA computation model.