# A Logic-Based Calculus of Fluents

This report formally defines the class of all problems on {\em
Reasoning about Actions and Change}, where accurate and complete
information about actions, together with strict inertia in continuous
time, continuous change and alternative results of possibly
concurrent and independent actions are the assumed properties. The
intended model set for each member in the class is defined in terms
of a model-theoretic trajectory semantics. The case is designated, in
the {\em Features and Fluents} framework, with the~\KRACi family of
reasoning problems. A fix-point characterization of the subclass
\KspRAdCi is then given in terms of a simulative algebraic semantics,
and show which are the difficulties when approaching the full class
with that method. A non-simulative algebraic semantics is then
presented as an alternative algebraic characterization of the
model-theoretic trajectory semantics. Still the characterization is
made in terms of complete lattices and continuous operators on those
complete lattices. The algebraic semantics is shown to be correct and
complete with respect to the trajectory-semantics, when applied to
reasoning problems in \KRACi. Finally, adopting the non-simulative
algebraic semantics as proof procedure, a logic-based {\em
Calculus~of~Fluents} is defined, via a meta-theoretic extension of
the Horn Clause Logic using the non-ground representation of object
level variables. The meta-interpreter consists in the Horn clause
representation of the proof procedure. The calculus is shown to be
decidable, domain independent and class dependent; its semantics
consists in the non-simulative algebraic semantics, and is executable
as a logic program by the SLD-resolution rule.