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.