basicstyle = , basewidth = 0.5em, moredelim = [s][] {} , moredelim = *[s][](),
literate = ,, 1
= \= 3 #< #< 4 #> #> 4 #= #= 3 #<> #<> 5 #=< #=< 5 #>= #>= 5 │$|\ $1  keywords
= , upquote = true, basicstyle = -0.5, basewidth = 0.48em, moredelim =
**[is][]‘‘, moredelim = *[s][]#pred., moredelim = *[s][]#show., moredelim =
*[s][]#hide., moredelim = *[s][](), moredelim = *[s][]’’, moredelim =
*[s][]:-., moredelim = *[s][]/**/, commentstyle = , morecomment=[l]%,
morecomment=[s]/**/, literate = |$\mid$1 │$\mid$1 [[1 ]]1
$1 &((1 &))1 &..0
=\=2
$1, keywords = , upquote = true, basicstyle = , basewidth = 0.52em, moredelim
= *[s][]:-., moredelim = *[s][]{}, moredelim = *[s][]’’, moredelim = *[s][](),
commentstyle = , morecomment=[l]%, literate = ++2 .=.#=3 .<.#<3 .>.#>3
.=<.#=<4 .>=.#>=4 .
=."5C=3
=\=3 ....2 ,,1  basicstyle = , breaklines = true, breakatwhitespace = true,
literate = {{1 }}1 :-:-4 ?-?-4 .=.#=3 .<.#<3 .>.#>3 .=<.#=<4 .>=.#>=4 .
=."5C=3
=\=3 ....2  March 2003 LABEL:firstpage\--LABEL:lastpage

# Modeling and Reasoning in Event Calculus
using Goal-Directed Constraint Answer Set Programming 111This paper is an
extended version of the work by Arias et al. (2019).††thanks: Work partially
supported by EIT Digital, MICINN projects RTI2018-095390-B-C33 InEDGEMobility
(MCIU/AEI/FEDER, UE), PID2019-108528RB-C21 ProCode, Comunidad de Madrid
project S2018/TCS-4339 BLOQUES-CM co-funded by EIE Funds of the European
Union, US NSF Grants IIS 1718945, IIS 1910131, IIP 1916206.

Joaquín Arias1 Manuel Carro2,3 Zhuo Chen4 Gopal Gupta4
1CETINIA Universidad Rey Juan Carlos 2IMDEA Software Institute
3Universidad Politécnica de Madrid 4University of Texas at Dallas
<EMAIL_ADDRESS>manuel.carro@{imdea.org,upm.es},
<EMAIL_ADDRESS>
(2003)

###### Abstract

Automated commonsense reasoning is essential for building human-like AI
systems featuring, for example, explainable AI. Event Calculus (EC) is a
family of formalisms that model commonsense reasoning with a sound, logical
basis. Previous attempts to mechanize reasoning using EC faced difficulties in
the treatment of the continuous change in dense domains (e.g., time and other
physical quantities), constraints among variables, default negation, and the
uniform application of different inference methods, among others. We propose
the use of s(CASP), a query-driven, top-down execution model for Predicate
Answer Set Programming with Constraints, to model and reason using EC. We show
how EC scenarios can be naturally and directly encoded in s(CASP) and how it
enables deductive and abductive reasoning tasks in domains featuring
constraints involving both dense time and dense fluents.

Under consideration in Theory and Practice of Logic Programming (TPLP)

###### doi:

S1471068401001193

##  1 Introduction

The ability to model continuous characteristics of the world is essential for
Commonsense Reasoning (CR) in many domains that require dealing with
continuous change: time, the height of a falling object, the gas level of a
car, the water level in a sink, etc. Event Calculus (EC) is a formalism based
on many-sorted predicate logic Kowalski and Sergot (1989); Mueller (2014) that
can represent continuous change and capture the commonsense law of inertia,
whose modeling is a pervasive problem in CR. In EC, time-dependent properties
and events are seen as objects and reasoning is performed on the truth values
of properties and the occurrences of events at a point in time.

Answer Set Programming (ASP) is a logic programming paradigm that was
initially proposed by Marek and Truszczynski (1999) and Lifschitz (1999) to
realize non-monotonic reasoning. ASP has been used by Lee and Palla (2012,
2020) to model the Event Calculus. Classical implementations of ASP are
limited to variables ranging over discrete and bound domains and use grounding
and SAT solving to find out models (called answer sets) of ASP programs.
However, reasoning on models of the real world often needs variables ranging
over dense domains (domains that are continuous, such as $\mathbb{R}$, or that
are not continuous but have an infinite number of elements in any bound, non-
singleton interval, such as $\mathbb{Q}$). Dense domains are necessary to
accurately represent the properties of some physical quantities, such as time,
weight, space, etc.

This paper presents an approach to modeling Event Calculus using the s(CASP)
system by Arias et al. (2018) as the underlying reasoning infrastructure. The
s(CASP) system is an implementation of Constraint Answer Set Programming over
first-order predicates which combines ASP and constraints. It features
predicates, constraints among non-ground variables, uninterpreted functions,
and, most importantly, a top-down, query-driven execution strategy. These
features make it possible to return answers with non-ground variables,
possibly including constraints among them, and to compute partial models by
returning only the fragment of a stable model that is necessary to support the
answer to a given query. Thanks to its interface with constraint solvers,
sound non-monotonic reasoning with constraints is possible. This approach
achieves more conciseness and expressiveness, in the sense of being able to
succinctly express complex computations and reasoning tasks, than other
related approaches. Dense domains can be faithfully modeled in s(CASP) as
continuous quantities, while in other proposals such domains had to be
discretized, as done by Mellarkod et al. (2008a) and Lee and Palla (2020),
therefore losing precision or even soundness. Additionally, in our approach
the amalgamation of ASP and constraints and its realization in s(CASP) is
considerably more natural: under s(CASP), answer set programs are executed in
a goal-directed manner so constraints encountered along the way are collected
and solved dynamically as execution proceeds --- this is very similar to the
way in which Prolog was extended with constraints. The implementation of other
ASP systems featuring constraints is considerably more complex.

In the rest of the paper we present s(CASP) and its unique capabilities
together with a terse introduction to Event Calculus (Section 2), our approach
to modeling Event Calculus with s(CASP) (Section 3), a quantitative and
qualitative evaluation (Section 4), and, finally, related work and conclusions
(Sections 5 and 6).

##  2 Background

Answer Set Programming is a logic programming and modelling language that
evaluates normal logic programs under the stable model semantics proposed by
Gelfond and Lifschitz (1988). s(ASP), introduced by Marple et al. (2017), is a
top-down, goal-driven ASP system that can evaluate ASP programs with function
symbols (_functors_) without _grounding_ them either before or during
execution. Grounding is a procedure that substitutes program variables with
the possible values from their domain. For most classical ASP solvers,
grounding is a necessary pre-processing phase. Grounding, however, requires
program variables to be restricted to take values in a finite domain. As a
result, traditional ASP solvers cannot be used to model continuous time or
change.

###  2.1 s(CASP)

s(CASP), presented by Arias et al. (2018), extends s(ASP) by adding
constraints, similarly to how CLP extends Prolog. Also, similarly to how
s(ASP) can compute the stable model semantics with non-ground programs and
return non-ground models including disequalities in the Herbrand domain,
s(CASP) keeps constraints as relations among variables both during execution
and in the answer sets.

Constraints have historically proved to be effective in improving both
expressiveness (programs are shorter and easier to understand, as many
computation details are taken care of by the underlying constraint solver) and
efficiency in logic programming, as they can succinctly express properties of
a solution and reduce the search space. As a result, s(CASP) is more
expressive and faster than s(ASP), while retaining the capability of executing
non-ground predicate answer set programs.

####  2.1.1 Syntax and Behavior

An s(CASP) program is a set of clauses of the following form:

a:-ca, b1, $\dots$, bm, not bm+1, $\dots$, not bn.

where a and b1, $\dots$, bn are atoms. An atom is either a propositional
variable or the expression p(t1, $\ldots$, tn) if p is an $n$-ary predicate
symbol and t1, $\ldots$, tn are terms. A term is either a variable xi or a
function symbol f of arity n, denoted as f/n, applied to $n$ terms, e.g.,
f(t1, t2, $\ldots$, tn), where each ti is in turn a term. A function symbol of
arity 0 is called a constant. Program variables are usually written starting
with an uppercase letter, while function and predicate symbols start with a
lowercase letter. Numerical constants are written solely with digits.222There
are additional syntactical conventions to separate variables and non-variables
that are of no interest here. Therefore, s(CASP) accepts terms with the same
conventions as Prolog: f(a, b) is a term, and so are f(g(X),Y) and [f(a)|Rest]
(to denote a list with head f(a) and tail Rest).

##### A note on terminology

ASP literature often uses the term _constraint_ to denote constructions such
as :- p, q, i.e., rules without head. They express that the conjunction of
atoms p $\land\allowbreak$ q cannot be true: either p, q, or both, have to be
false in any stable model. Our programs use as well a designated class of
predicates that restrict the domains of variables Marriott and Stuckey (1998);
Marriott et al. (2006) and whose semantics comes from the structure and domain
of an underlying constraint system. In Constraint Logic Programming (CLP),
these predicates are called ‘‘constraints’’ as well. To avoid the ambiguity
that may arise from using the same name for constraints appearing among (free)
variables during program execution and in the final models and for rules
without heads, and following Mellarkod et al. (2008b), we will refer to
headless rules as _denials_.

ca is a simple constraint or a conjunction of constraints: an expression
establishing relations among variables in some constraint system, as described
by Marriott and Stuckey (1998). Similar to CLP, s(CASP) is parametrized by the
constraint system, from which it inherits its semantics. Since the execution
of an s(CASP) program needs negating constraints (Section 2.1.3), we require
that this can be done in the constraint system by means of a finite
disjunction of basic constraints Stuckey (1991); Dovier et al. (2000).

At least one of a, bi, not bi, or ca must be present. When the head a is not
present it is supposed to be substituted by the head _false_. The rules have
then the form

:-ca, b1, $\dots$, bm, not bm+1, $\dots$, not bn.

(and, as mentioned before, we call this rule a _denial_) and their
interpretation is that the conjunction of the constraints and goals has to be
false, so at least one constraint or goal has to be false.

The execution of an s(CASP) program starts with a _query_ of the form

?- ca, b1, $\dots$, bm, not bm+1, $\dots$, not bn.

The s(SCASP) answers to a query are _partial_ stable models where each one is
a subset of a stable model that satisfies the constraints, makes non-negated
atoms true, makes the negated atoms non-provable, and, in addition, includes
only atoms that are relevant to support the query. Additionally, for each
partial stable model s(CASP) can return on backtracking the justification tree
and the bindings for the free variables of the query that correspond to the
most general unifier (_mgu_) of a successful top-down derivation consistent
with this stable model.

An atom can have the form -r (i.e., have a hyphen as its first character). In
that case it is assumed to express the _classical negation_ of atom r. Rules
with head -r, to express when r is false, can be part of the program. To
ensure soundness, a denial

:- r, -r.

is automatically added to guarantee that atom r and its classical negation -r
are not both simultaneously true in any model. Other than that, -r is not
treated specially by s(CASP). The construct not -r is allowed and rules with
-r in their head or body are subject to _dualization_ (Section 2.1.3).

Default negation not r differs from classical negation -r in that not r
succeeds when it cannot be proven from the program that r holds, while -r
succeeds if there is a rule that states how to deduce -r and this rule,
together with the rest of the program, can be used to derive -r. The
difference from the point of view of reasoning can be illustrated with a
simple piece of commonsense knowledge: a bus may cross the railway tracks if
no train is approaching. A possible rule using classical negation expresses
would be:

cross:- -train.

It means the railway tracks can be crossed if we _explicitly_ know (because
there is a proof for it) that no train is approaching \--- for example,
because there are sensors that send us information that ensures that there is
definitely no train on the tracks within some safety range. The rule using
default negation would be:

cross:- not train.

which means that we can cross the railway tracks if there is no evidence
(because we cannot prove it) that a train is approaching \--- for example, we
do not receive information of a train coming. But there may be no train
coming, or the sensors may be faulty and not sending signals. That is why -r
is sometimes referred to as _strong_ negation: it carries with it the meaning
that there is a constructive proof that r is false. Therefore, lack of
evidence is not a hard proof. Classical and default negation have two
different meanings inside the language and are used to express very different
common-sense reasoning scenarios.

When -r and r are defined, the decision to invoke -r or not r in the body a
rule depends on what the programmer wants to express. There is a relation of
containment between not r and -r, but it is clearer in the context of non-
propositional atoms. Therefore, we defer its explanation to the end of Section
3.4, when we deal with the translations of the axioms of the Basic Event
Calculus (BEC).

In s(CASP), and unlike Prolog’s negation as failure and ASP default negation,
not p(X) can return bindings for X on success, i.e., bindings for which the
call p(X) would have failed. Constraints may be returned as well: for the
program

⬇

1p(a).

the query ?- not p(X). would return the binding X $\not=$ a and the model {not
p(X ${X$\not=$a})$|, representing the set of $not\;p(X)$ such that the atom
$p(X)$ can be proven only when $X\not=a$.333Uniqueness of names is assumed for
constants and function names: any two constants or functions with different
names represent different objects. Note that X in the query appeared only in a
negated atom, and did not need to be part of any non-negated atom. This is
possible thanks to the use of constructive negation Marple et al. (2017) and
coinductive success Gupta et al. (2007) in s(ASP).

These are augmented in s(CASP) with the constraint processing capabilities
presented in Arias et al. (2018), such that the program

⬇

1p(X):- X > 0.

will return, for the same query as before, the model {not p(X ${X$\leq$0})$|.

s(CASP) uses a top-down, goal-driven execution procedure that implements an
extension of the stable model semantics introduced by Gelfond and Lifschitz
(1988) for non-ground programs. Default negation is solved against the _dual
rules_ of the program, which give a constructive definition of the negation of
program predicates. The top-down algorithm does not need grounded programs and
makes it possible as well to return partial stable models.

####  2.1.2 Overview of the Execution Procedure of s(CASP)

In the following sections we will present an abridged description of the top-
down evaluation procedure used by s(CASP), which, in a nutshell, is:

  1. 1.

Rules expressing the constructive negation of the predicates in the original
ASP program are synthesized (Section 2.1.3). We call this the _dual program_.
Its mission is to provide a means to constructively determine the conditions
and constraints under which calls to non-propositional predicates featuring
variables would have failed: if we want to know when a rule such as p(X, Y):-
q(X), not r(Y). succeeds, the dual program computes the constraints on Y under
which the call r(Y) would fail. This is an extension of the usual ASP
semantics that is compatible with the case of programs that can be finitely
grounded.444Note that, in the presence of function symbols and constraints on
dense domains, this is in general not the case for s(CASP) programs.

  2. 2.

The original program is checked for loops of the form p:- q, not p. and
denials are generated for them.

  3. 3.

The denials generated in point 2, together with any denials present in the
original program, are collected in a predicate synthesized by the compiler
that is invoked by adding an auxiliary goal to this predicate at the end of
the query.

  4. 4.

The union of the original program, the dual program, and the denials is
handled by a top-down execution algorithm that implements the stable model
semantics.

Item number 4 is specially relevant. The dual program (item 1) is synthesized
by means of program transformations drawing from classical logic. However, its
meaning differs from that of first-order logic. That is so because it is to be
executed by a metainterpreter that does not implement the inference mechanisms
of first-order logic, as it is designed to ensure that the semantics of answer
set programs is respected. In particular, it treats specifically cyclic
dependencies involving negation --- see Section 2.1.4. For conciseness, we
have not included in this paper the description of the execution algorithm,
which can be found in Marple et al. (2012) and Marple et al. (2017).

Therefore, the soundness of s(CASP) (and its version without constraints,
s(ASP)) needs to be assessed taking into account the dual program, the
generation of the denials and the evaluation algorithm as a whole. This was
done by Marple et al. (2012) for the propositional case (which lays the bases
of the whole procedure) and extended for the case of predicate logic,
including arbitrary function symbols, by Marple et al. (2017). We will provide
reasons supporting the soundness of the s(CASP) algorithm in the next
sections.

####  2.1.3 Dual Programs

We summarize here the synthesis of the dual of a logic program $P$: the
completion procedure described by Clark (1978) is performed to generate a
program $Comp(P)$, its rules are converted into an equivalent form with
negated heads, and then De Morgan’s laws are applied to generate separate
clauses.

  1. 1.

Following Ferraris et al. (2011, Section 2.1), first-order sentences are
constructed for each clause by considering each i-th rule of predicate $p$

p :- ca, b1, $\dots$, bm, not bm+1, $\dots$, not bn.

as a shorthand for $\forall\vec{x}\vec{y_{i}}\;(p_{i}(\vec{x})\leftarrow
B_{i})$, where $B_{i}$ corresponds to the conjunction $c_{a}\land\allowbreak
b_{1}\land\allowbreak\dots\land\allowbreak b_{m}\land\allowbreak\neg
b_{m+1}\land\allowbreak\dots\land\allowbreak\neg b_{n}$ and $\vec{y_{i}}$ are
the variables appearing in $B_{i}$ that do not appear in $\vec{x}$. The
rationale for this transformation is that the grounding of an ASP program
substitutes variables in the program clauses for all the constants in the
program, and all the resulting clauses have to be satisfied. This is precisely
what the universal quantifier expresses.

We will assume that clauses are normalized, i.e. head unifications have been
made explicit as goals in the bodies of the corresponding clauses and the
heads contain only variable names. Also, in what follows we will not
distinguish user predicates bi from constraints ca until the last step of the
generation of the dual program; we will make the necessary distinction there.

  2. 2.

All sentences corresponding to the same predicate name are conjoined together:

$\displaystyle\forall\vec{x}\vec{y_{i}}\;(p(\vec{x})\leftarrow
B_{1})\;\land\allowbreak$ $\displaystyle\vdots$
$\displaystyle\forall\vec{x}\vec{y_{k}}\;(p(\vec{x})\leftarrow B_{k})$

  3. 3.

The bodies in the antecedent of the sentences are joined in a single body:

$\forall\vec{x}\vec{y}\;(p(\vec{x})\leftarrow
B_{1}\lor\allowbreak\dots\lor\allowbreak B_{k})$

The variables $\vec{y}$ are updated to include all $\vec{y_{i}}$ that appear
in the different $B_{i}$ and do not appear in $\vec{x}$.

  4. 4.

The scope of the quantifiers is minimized to make further simplifications
possible:

$\forall\vec{x}\;(p(\vec{x})\leftarrow\exists\vec{y}(B_{1}\lor\allowbreak\dots\lor\allowbreak
B_{k}))$

and then

$\forall\vec{x}\;(p(\vec{x})\leftarrow\exists\vec{y_{1}}B_{1}\lor\allowbreak\dots\lor\allowbreak\exists\vec{y_{k}}B_{k})$

Transformations 2 to 4 are valid in intuitionistic logic, and so they preserve
the stable models of the original formulae, as mentioned by Ferraris et al.
(2011, Section 6.1).

  5. 5.

Implications are replaced by equivalences, to generate the Clark completion of
the original predicate:

$\forall\vec{x}\;(p(\vec{x})\longleftrightarrow\exists\vec{y_{1}}B_{1}\lor\allowbreak\dots\lor\allowbreak\exists\vec{y_{k}}B_{k})$

This transformation is, in general, not model-preserving, except in the case
of tight programs as presented by Erdem and Lifschitz (2003). For a program
$P$, positive loops makes the Clark completion $Comp(P)$ under the classical
first-order semantics be weaker than $P$ under the stable model semantics: all
stable models of $P$ are classical models of $Comp(P)$, but not the other way
around. Therefore, there may be classical models of $Comp(P)$ that are not
stable models of $P$.

  6. 6.

We create new predicate names to separate the bodies corresponding to the
different original clauses:

$\displaystyle\forall\vec{x}\ (\ p(\vec{x})\longleftrightarrow
p_{1}(\vec{x})\lor\allowbreak\dots\lor\allowbreak p_{k}(\vec{x})\ )$
$\displaystyle\forall\vec{x}\ (\
p_{i}(\vec{x})\longleftrightarrow\exists\vec{y_{i}}B_{i})$

  7. 7.

Their duals $\lnot p/n$, $\lnot p_{i}/n$ are:

$\displaystyle\forall\vec{x}\ (\ \lnot
p(\vec{x})\longleftrightarrow\lnot(p_{1}(\vec{x})\lor\allowbreak\dots\lor\allowbreak
p_{k}(\vec{x}))\ )$ $\displaystyle\forall\vec{x}\ (\ \lnot
p_{i}(\vec{x})\longleftrightarrow\lnot\ \exists\vec{y}_{i}B_{i}\ )$

This is a semantically-preserving operation in the classical logic semantics,
and so the models of the Clark completion remain untouched.

  8. 8.

De Morgan’s laws are applied to the first formula (the ‘‘entry point’’ of the
negated predicate) and the existential quantifier is negated:

$\displaystyle\forall\vec{x}\ (\ \lnot p(\vec{x})\longleftrightarrow\lnot
p_{1}(\vec{x})\land\allowbreak\dots\land\allowbreak\lnot p_{k}(\vec{x})\ )$
$\displaystyle\forall\vec{x}\ (\ \lnot
p_{i}(\vec{x})\longleftrightarrow\forall\vec{y}_{i}\neg B_{i}\ )$

De Morgan’s Law are of course semantics-preserving in classical logic, but
also in the stable model semantics because the formulas
$\neg(A\land\allowbreak B)$ and $\neg A\lor\allowbreak\neg B$ are strongly
equivalent, as mentioned by Lifschitz et al. (2001, Proposition 5).

  9. 9.

For each dual rule corresponding to each $p_{i}$, an auxiliary _negated_
predicate corresponding to the _negated_ body is synthesized:

$\displaystyle\forall\vec{x}\ (\ \lnot p(\vec{x})\longleftrightarrow\lnot
p_{1}(\vec{x})\land\allowbreak\dots\land\allowbreak\lnot p_{k}(\vec{x})\ )$
$\displaystyle\forall\vec{x}\ (\ \lnot
p_{i}(\vec{x})\longleftrightarrow\forall\vec{y}_{i}\neg
p^{\prime}_{i}(\vec{x},\vec{y}_{i})\ )$ $\displaystyle\forall\vec{x}\vec{y}\
(\ \lnot p^{\prime}_{i}(\vec{x},\vec{y})\longleftrightarrow\neg B_{i}\ )$

Let us remember that each $B_{i}$ has the form
$b_{i,1}\land\allowbreak\dots\land\allowbreak b_{i,m}\land\allowbreak\lnot\
b_{i,m+1}\land\allowbreak\dots\land\allowbreak\lnot\ b_{i,n}$. Therefore, the
last sentence is

$\forall\vec{x},\vec{y}\ (\ \lnot
p^{\prime}_{i}(\vec{x},\vec{y})\longleftrightarrow\neg(b_{i,1}\land\allowbreak\dots\land\allowbreak
b_{i,m}\land\allowbreak\lnot\
b_{i,m+1}\land\allowbreak\dots\land\allowbreak\lnot\ b_{i,n})\ )$

  10. 10.

We apply De Morgan’s Law to the last sentence in the previous point to obtain

$\displaystyle\forall\vec{x},\vec{y}\ (\ \lnot
p^{\prime}_{i}(\vec{x},\vec{y})\longleftrightarrow\neg
b_{i,1}\lor\allowbreak\dots\lor\allowbreak\neg b_{i,m}\lor\allowbreak
b_{i,m+1}\lor\allowbreak\dots\lor\allowbreak b_{i,n}\ )$

  11. 11.

We revert the introduction of the equivalence. This transformation changes the
models of program w.r.t. that of the Clark completion. However, programs under
the stable semantics (and under Prolog semantics) have a clear notion of
direction and the metainterpreter only uses the goal-driven direction ‘‘use
_Body_ to prove _Head_ ’’. The closed-world assumption, captured by Clark’s
completion, is already implicit in the top-dow evaluation algorithm of
s(CASP).

$\displaystyle\forall\vec{x}\ (\ \lnot p(\vec{x})\leftarrow\lnot
p_{1}(\vec{x})\land\allowbreak\dots\land\allowbreak\lnot p_{k}(\vec{x})\ )$
$\displaystyle\forall\vec{x}\ (\ \lnot
p_{i}(\vec{x})\leftarrow\forall\vec{y}_{i}\neg
p^{\prime}_{i}(\vec{x},\vec{y}_{i})\ )$ $\displaystyle\forall\vec{x}\vec{y}\
(\ \lnot p^{\prime}_{i}(\vec{x},\vec{y})\leftarrow\neg
b_{i,1}\lor\allowbreak\dots\lor\allowbreak\neg b_{i,m}\lor\allowbreak
b_{i,m+1}\lor\allowbreak\dots\lor\allowbreak b_{i,n})\ )$

  12. 12.

Separate the disjunction in the body of the last sentence in different
clauses:

$\displaystyle\forall\vec{x}\vec{y}\ (\ \lnot
p^{\prime}_{i}(\vec{x},\vec{y})\leftarrow\neg b_{i,1}\ )$
$\displaystyle\forall\vec{x}\vec{y}\ (\ \lnot
p^{\prime}_{i}(\vec{x},\vec{y})\leftarrow\neg b_{i,2}\ )$
$\displaystyle\vdots$ $\displaystyle\forall\vec{x}\vec{y}\ (\ \lnot
p^{\prime}_{i}(\vec{x},\vec{y})\leftarrow b_{i,n}\ )$

These clauses, together with the original program and the denials, are used by
the metainterpreter to decide whether some atom belongs or not to a stable
model of a program and to return the (minimal) support for that atom.

This provides a definition for $\lnot p(\vec{x})$ via a clause with head
$\lnot p_{i}(\vec{x})$ for each original clause with head $p_{i}(\vec{x})$.
The newly introduced negated atoms $\neg b_{i.1}\ldots\neg b_{1.m}$ can fall
into two categories: they are either negations of user predicates or negations
of constraints. In the former case, the procedure just described generates a
definition for the negation of user predicates. In the latter case,
constraints are either head unifications created after normalizing the
clauses, or they are constraints in a different domain. Both cases are treated
similarly:

  * •

If the negation of a constraint can be expressed as a finite disjunction of
basic constraints Dovier et al. (2000); Stuckey (1991), the compiler makes
that expansion. In the simplest case, that disjunction is a single constraint:
a linear constraint $E_{1}<E_{2}$ is translated into $E_{1}\geq E_{2}$. In
other cases, it can be a ‘‘real’’ disjunction: the constraint $E_{1}=E_{2}$ in
CLP($\mathbb{Q}$) (linear constraints over the rationals), is negated by
converting it into $E_{1}<E_{2}\lor\allowbreak E_{1}>E_{2}$, and each
component of the disjunction is handled by a clause. In practice, it is not
necessary that all constraints in a constraint system can be negated, but only
those that are required in a given program to answer some query.

  * •

When the negation of a constraint cannot be expressed as a finite disjunction
of constraints, we make a best effort to provide an _ad-hoc_ implementation.
For example, for the equalities $v_{i}=t_{i}$ in the Herbrand domain
CLP($\mathcal{H}$) that were added when normalizing clauses, we introduce a
call $\mathit{diff}(v_{i},t_{i})$ to a disequality solver provided by the
runtime environment. Negation of equality in CLP($\mathcal{H}$) can be
expressed as a finite disjunction only for programs that can generate a finite
number of ground terms.

Executable code for the dual program is generated by removing the external
quantifiers (as in Horn clauses) and translating the universal quantifiers
that were applied to local variables into a call to the predicate forall(Var,
Pred), provided by the s(CASP) runtime.

###### Example 1

Given the program

⬇

1p(X):- q(X, Z), not r(X).

2p(Z):- not q(X, Z), r(X).

3q(X, a):- X .>. 5.

4r(X):- X .<. 1.

its dual is shown below

⬇

1% not p/1

2not p(A) :- not p_1(A), not p_2(A).

3

4not p_1(A) :- forall(B, not p_1(A,B)).

5not p_1(A,B) :- not q(A,B).

6not p_1(A,B) :- r(A).

7

8not p_2(A) :- forall(B, not p_2(A,B)).

9not p_2(A,B) :- q(B,A).

10not p_2(A,B) :- not r(B).

11% not q/1

12not q(A,B) :- not q_1(A,B).

13

14not q_1(A,B) :- B \= a.

15not q_1(A,B) :- A #=< 5.

16

17% not r/1

18not r(A) :- not r_1(A).

19not r_1(A) :- A #>= 1.

####  2.1.4 Sketch of the Execution Scheme

Queries to the original program extended with the dual rules are evaluated by
a runtime environment. This is currently a metainterpreter written in Prolog
that executes the algorithm described by Marple et al. (2012). This algorithm
has similarities with SLD resolution, but it takes into account specific
characteristics of ASP and the dual programs, such as the different kinds of
loops, the denials, and the introduction of universal quantifiers in the body
of the clauses. The main highlights of this algorithm are:

Loop handling:

Two different cases are distinguished by Marple et al. (2012):

  * •

When a call eventually invokes itself and there is an odd number of
intervening negations (as in, e.g., p:- q. q:- not r. r:- p.), the evaluation
fails (and backtracks) to avoid contradictions of the form
$p\land\allowbreak\lnot p$.

  * •

When there is an even number of intervening negations, as in p:- not q. q:- r.
r:- not p. the metainterpreter generates several stable models, such as {p,
not q, not r} and {q, r, not p}.

Denials:

The s(CASP) compiler automatically generates an auxiliary predicate that
captures all the denials written by the programmer. This predicate is invoked
during query evaluation to ensure that the returned models are consistent with
the denials. The current implementation executes them at the end of the query
evaluation, when a candidate model has been generated. It would however be
possible to check them at appropriate points while the execution proceeds, in
order to increase performance, as suggested by Marple and Gupta (2014).

The s(CASP) compiler also detects statically rules of the form r:-q, not r.
and introduces denials to ensure that the models satisfy $\lnot
q\lor\allowbreak r$, even if the atoms r or q are not needed to solve the
query. This is done by building a dependency graph of the program and
detecting the paths where this may happen, including across several calls. For
the propositional case, such an analysis can be precise. For the non-
propositional case, an over-approximation is calculated. In both cases,
denials that are not used during program evaluation can be generated. These
may impose a penalty in execution time, but are safe. Therefore, s(CASP) will
state that the program

⬇

1p :- not q.

2q :- not p.

3r :- not r.

has no stable models, regardless of the initial query.

Universal quantification:

Universal quantifications in the body of the clauses are translated into the
construction forall(Var, Pred). This is implemented by the runtime environment
by solving Pred, extracting the constraints attached to the quantified
variables, and using these constraints negated to narrow the constraint store
under which Pred is executed. This is iterated until failure or until the
constraint store has an empty domain for the quantified variables. Arias et
al. (2018) present this algorithm in more detail.

####  2.1.5 Execution with Unsafe Variables and Uninterpreted Function Symbols

The code in Example 1 has variables that would be termed as _unsafe_ in
regular ASP systems: variables that appear in negated atoms in the body of a
clause, but that do not appear in any positive literal in the same body. Since
s(CASP) synthesizes explicit constructive goals for these negated goals, the
aforementioned code can be run as-is in s(CASP). The query ?- p(A). generates
three different models:

⬇

{ p(A | {A $>$ 5}), q(A | {A $>$ 5}, a), not r(A | {A $>$ 5}) }

A $>$ 5

{ p(A | {A $\not=$ a}), not q(B | {B $<$ 1}, A | {A $\not=$ a}), r(B | {B $<$ 1}) }

A $\not=$ a

{ p(a), not q(B | {B $<$ 1}, a), r(B | {B $<$ 1}) }

A = a

where the notation V | {C} for a variable V is intended to mean that V is subject to the constraints in {C}. The constraints A = 5, A $\not=$ a, and A = a correspond to the bindings of variable A that make the atom in the query ?- p(A) belong to the stable model.

Another very relevant point where s(CASP) differs from ASP is in the
possibility of using arbitrary uninterpreted function symbols to build, for
example, data structures. While in mainstream ASP implementations these could
give rise to an infinite grounded program, the s(CASP) execution model can
deal with them similarly to Prolog, with the added power of the use of
constructive negation in the execution and in the returned models.

###### Example 2

The predicate member/2 below models the membership to a list as it is usual in
(classical) logic programming. The query is intended to derive the conditions
for one argument not to belong to a given list.

⬇

1member(X, [X|Xs]).

2member(X, [_|Xs]):- member(X, Xs).

3

4list([1,2,3,4,5]).

5

6?- list(A), not member(B, A).

This program and query return in s(CASP) the following model and binding:

⬇

{ list([1,2,3,4,5]),

not member(B | {B $\not=$ 1,B $\not=$ 2,B $\not=$ 3,B $\not=$ 4,B $\not=$ 5}, [1,2,3,4,5]),

not member(B | {B $\not=$ 1,B $\not=$ 2,B $\not=$ 3,B $\not=$ 4,B $\not=$ 5}, [2,3,4,5]),

not member(B | {B $\not=$ 1,B $\not=$ 2,B $\not=$ 3,B $\not=$ 4,B $\not=$ 5}, [3,4,5]),

not member(B | {B $\not=$ 1,B $\not=$ 2,B $\not=$ 3,B $\not=$ 4,B $\not=$ 5}, [4,5]),

not member(B | {B $\not=$ 1,B $\not=$ 2,B $\not=$ 3,B $\not=$ 4,B $\not=$ 5}, [5]),

not member(B | {B $\not=$ 1,B $\not=$ 2,B $\not=$ 3,B $\not=$ 4,B $\not=$ 5}, []) }

A = [1,2,3,4,5], B $\not=$ 1, B $\not=$ 2, B $\not=$ 3, B $\not=$ 4, B $\not=$
5

I.e., for variable B not to be a member of the list [1,2,3,4,5] it has to be
different from each of its elements.

In addition to default negation, s(CASP) supports classical negation to
capture the explicit evidence that a literal is false, as mentioned in Section
2.1.1.

s(CASP) is implemented in Ciao Prolog Hermenegildo et al. (2012) and is
available at https://gitlab.software.imdea.org/ciao-lang/scasp.

####  2.1.6 s(CASP) as a Conservative Extension of ASP

The behavior of s(CASP) and ASP is the same for propositional programs. For
programs featuring unsafe variables (legal in ASP, but not in mainstream ASP
systems) or programs that could create data structures arbitrarily large or
whose variable ranges are defined in infinite domains (either unbound or bound
but dense), which are outside the standard domain of ASP systems as they
cannot be finitely grounded, s(CASP) extends ASP in a consistent way. The
domain of the variables is implicitly expanded to include a domain which can
be potentially infinite.

Let us use an example introduced in (Marple et al., 2017, Pag.12). We are
interested in knowing whether p(X) (for some X) is or not part of a stable
model:

⬇

1d(1).

2p(X) :- not d(X).

The only constant in the program is 1, which is the only possible domain for X
in the second clause. That clause is not legal for ASP, as X is an unsafe
variable (Sect. 2.1.5). Adding a domain predicate call for it (i.e., adding
d(X) to the body of the second clause), makes its model be {d(1)} (not p(1) is
implicit).

That second clause is however legal in s(CASP). Making the query ?-p(X)
returns the _partial_ model {p(X|{X \= 1}), not d(X|{X \= 1})} stating that
p(X) and not d(X) are true when X \= 1, which is consistent with, but more
general than, the model given by ASP. As the model is partial, only the atoms
(perhaps negated) involved in the proof for ?- p(X) appear in that model.

###  2.2 Circumscription

_Circumscription_ McCarthy (1980); Lifschitz (1985) is a technique to perform
non-monotonic reasoning within the framework of first-order logic.
Circumscription minimizes the extension555The _extension_ of a predicate is
the set of tuples for which predicate is true. of the predicates that we want
to circumscribe. Intuitively, it aims at formalizing that the known objects in
a certain class are _all_ the objects that are in that class. Event Calculus
theories require that some of their predicates are circumscribed to ensure
that they can only be interpreted as they appear in the description of the
scenario.

The following definition of circumscription is due to Lifschitz (1985):

######  Definition 1 (Circumscription)

Let $A(P,Z)$ denote a sentence, where $P$ is a tuple of predicate constants
and $Z$ a tuple of function and/or predicate constants disjoint with $P$. The
circumscription of $P$ in $A(P,Z)$ with variable $Z$ is defined as the second
order sentence $A(P,Z)\land\allowbreak\neg\exists p,z(A(p,z)\land\allowbreak
p\mathbf{<}P)$. The $\mathbf{<}$ symbol in the previous expression is defined
as follows: if $U$ and $V$ are n-ary predicates, $U\mathbf{\leq}V$ stands for
$\forall x_{1}\ldots x_{n}(U(x_{1},\ldots,x_{n})\rightarrow
V(x_{1},\ldots,x_{n}))$. $U=V$ stands for $U\mathbf{\leq}V$ and
$V\mathbf{\leq}U$ and $U\mathbf{<}V$ stands for
$U\mathbf{\leq}V\land\allowbreak\neg(V\mathbf{\leq}U)$. These definitions are
extended to tuples of predicates in the obvious fashion.

$U\mathbf{\leq}V$ expresses that the extension of $U$ is a subset of the
extension of $V$, and $U\mathbf{<}V$ means that the extension of $U$ is a
proper subset of the extension of $V$. The circumscription of $A(P,Z)$ is a
formula whose extension is the minimal extension of the predicates in $P$ that
makes $A(P,Z)$ true, and in which the objects in $Z$ are allowed to vary. It
is expressed with $CIRC(A;P;Z)$ or $CIRC(A;P)$ if $Z$ is empty.

###### Example 3

Let’s take $A=P(a)$. Its minimization should express that $P$ is only true for
$a$:

$CIRC(A;P)\equiv\forall x(P(x)\leftrightarrow x=a)$

###### Example 4

Let’s take $A=\neg P(a)$. We only have information about $P$ not being true in
$a$, which is the only constant that appears in $A$, but also _all_ the
constants that appear in the sentence. Its minimization expresses this as:

$CIRC(A;P)\equiv\forall x\neg P(x)$

Computing circumscriptions is in general a hard task. However, there are class
of formulas (_separable formulas_) for which it has shown to be easy by
Lifschitz (1985). Also, Ferraris et al. (2011) have shown that there is a
close relationship between circumscription and stable models and indeed Lee
and Palla (2012, Definition 2) proved that the stable model semantics
coincides with the circumscription for a large class of formulas called
_canonical formulas_. Non-canonical formulas can often be rewritten as
canonical formulas, therefore expanding the range of coincidence of
circumscription and stable model semantics.

###  2.3 Event Calculus

Predicate |  Meaning
---|---
$\mathit{InitiallyN}(f)$ |  fluent $f$ is false at time 0
$\mathit{InitiallyP}(f)$ |  fluent $f$ is true at time 0
$\mathit{Happens}(e,t)$ |  event $e$ occurs at time $t$
$\mathit{Initiates}(e,f,t)$ |  if $e$ happens at time $t$, $f$ is true and not released from the commonsense law of inertia after $t$
$\mathit{Terminates}(e,f,t)$ |  if $e$ occurs at time $t$, $f$ is false and not released from the commonsense law of inertia after $t$
$\mathit{Releases}(e,f,t)$ |  if $e$ occurs at time $t$, $f$ is released from the commonsense law of inertia after $t$
$\mathit{Trajectory}(f_{1},t_{1},f_{2},t_{2})$ |  if $f_{1}$ is initiated by an event that occurs at $t_{1}$, then $f_{2}$ is true at $t_{2}$
$\mathit{StoppedIn}(t_{1},f,t_{2})$ |  $f$ is stopped between $t_{1}$ and $t_{2}$
$StartedIn(t_{1},f,t_{2})$ |  $f$ is started between $t_{1}$ and $t_{2}$
$\mathit{HoldsAt}(f,t)$ |  fluent $f$ is true at time $t$

Figure 1: Basic event calculus (BEC) predicates

($e$ = event, $f$, $f_{1}$, $f_{2}$ = fluents, $t$, $t_{1}$, $t_{2}$ =
timepoints)

EC (presented at length by, for example, Mueller (2014)) is a formalism for
reasoning about events and change, of which there are several axiomatizations.
There are three basic, mutually related, concepts in EC: _events_ , _fluents_
, and _time points_. An event is an action or incident that may occur in the
world: for instance, a person dropping a glass is an event. A fluent is a
time-varying property of the world, such as the altitude of a glass. A time
point is an instant in time. Events may happen at a time point; fluents have a
truth value at any time point or over an interval, and their truth values are
subject to change upon the occurrence of an event. In addition, fluents may
have (continuous) quantities associated with them when they are true.

For example, the status of a glass falling may be represented by two fluents:
one that captures the fact that the glass is falling and another one that
captures the height of the glass over the ground. The _event_ of dropping a
glass initiates the _fluent_ that captures that the glass is falling and gives
some initial value to its height. This height changes with time according to
some formula. The event of catching the glass makes the fluent that reflects
it is falling false and makes its height not to change, possibly until a
further event takes place. An EC description consists of a domain narrative
(Fig. 1) and a universal theory (Fig. 2). The domain narrative consists of the
causal laws of the domain, the known events, and the fluent properties, and
the universal theory is a conjunction of EC axioms that encode, for example,
the inertia laws.

The original EC (OEC) was introduced by Kowalski and Sergot (1989). OEC has
sorts for event occurrences, fluents, and time periods. In this paper we use
the Basic Event Calculus (BEC) formulated by Shanahan (1999) as presented by
Mueller (2008a). BEC allows fluents to be released from the commonsense law of
inertia via the $Release$ predicate, and adds the ability to represent
continuous change via the $Trajectory$ predicate. Fig. 2 summarizes the seven
axioms of the BEC theory. An explanation of these axioms follows:

BEC1. | $\mathit{StoppedIn}(t_{1},f,t_{2})\ \ \equiv$ |
---|---|---
$\exists e,t\ \ (\ \mathit{Happens}(e,t)\land\allowbreak
t_{1}<t<t_{2}\land\allowbreak(\
\mathit{Terminates}(e,f,t)\lor\allowbreak\mathit{Releases}(e,f,t)\ )\ )$
BEC2. | $\mathit{StartedIn}(t_{1},f,t_{2})\ \ \equiv$ |
$\exists e,t\ \ (\ \mathit{Happens}(e,t)\land\allowbreak
t_{1}<t<t_{2}\land\allowbreak(\
\mathit{Initiates}(e,f,t)\lor\allowbreak\mathit{Releases}(e,f,t)\ )\ )$
BEC3. | $\mathit{HoldsAt}(f_{2},t_{2})\ \ \leftarrow$ |
$\mathit{Happens}(e,t_{1})\land\allowbreak\mathit{Initiates}(e,f_{1},t_{1})\land\allowbreak\mathit{Trajectory}(f_{1},t_{1},f_{2},t_{2})\land\allowbreak\lnot\mathit{StoppedIn}(t_{1},f_{1},t_{2})$
BEC4. |  $\mathit{HoldsAt}(f,t)\ \ \leftarrow$ $\mathit{InitiallyP}(f)\land\allowbreak\lnot\mathit{StoppedIn}(0,f,t)$
BEC5. |  $\lnot\mathit{HoldsAt}(f,t)\ \ \leftarrow$ $\mathit{InitiallyN}(f)\land\allowbreak\lnot\mathit{StartedIn}(0,f,t)$
BEC6. | $\mathit{HoldsAt}(f,t_{2})\ \ \leftarrow$ |
$\mathit{Happens}(e,t_{1})\land\allowbreak\mathit{Initiates}(e,f,t_{1})\land\allowbreak
t_{1}<t_{2}\land\allowbreak\lnot\mathit{StoppedIn}(t_{1},f,t_{2})$
BEC7. | $\lnot\mathit{HoldsAt}(f,t_{2})\ \ \leftarrow\ \ $ |
$\mathit{Happens}(e,t_{1})\land\allowbreak\mathit{Terminates}(e,f,t_{1})\land\allowbreak
t_{1}<t_{2}\land\allowbreak\lnot\mathit{StartedIn}(t_{1},f,t_{2})$
Figure 2: Formalization of BEC theory as presented by Mueller (2014).

  * •

Axiom BEC1. A fluent $f$ is stopped between time points $t_{1}$ and $t_{2}$
iff it is terminated or released by some event $e$ that occurs after $t_{1}$
and before $t_{2}$.

  * •

Axiom BEC2. A fluent $f$ is started between time points $t_{1}$ and $t_{2}$
iff it is initiated or released by some event $e$ that occurs after $t_{1}$
and before $t_{2}$.

  * •

Axiom BEC3. A fluent $f_{2}$ is true at time $t_{2}$ if a fluent $f_{1}$
initiated at $t_{1}$ does not finish before $t_{2}$ and it makes fluent
$f_{2}$ be true.666For implementation convenience, and without loss of
expressiveness, we assume that argument $t_{2}$ in
$Trajectory(f_{1},t_{1},f_{2},t_{2})$ is not a time difference w.r.t. $t_{1}$,
but an absolute time after $t_{1}$.

  * •

Axiom BEC4. A fluent $f$ is true at time $t$ if it is true at time 0 and is
not stopped on or before $t$.

  * •

Axiom BEC5. A fluent $f$ is false at time $t$ if it is false at time 0 and it
is not started on or before $t$.

  * •

Axiom BEC6. A fluent $f$ is true at time $t_{2}$ if it is initiated at some
earlier time $t_{1}$ and it is not stopped before $t_{2}$.

  * •

Axiom BEC7. A fluent $f$ is false at time $t_{2}$ if it is terminated at some
earlier time $t_{1}$ and it is not started on or before $t_{2}$.

##  3 From Event Calculus to s(CASP)

###  3.1 Circumscription in s(CASP)

Circumscription is applied to EC domain narratives, and as a result, the
events that happen and their effects are only those explicitly defined. As
mentioned before, the definition of a given scenario (its _narrative_ part)
states the basic actions and effects using the predicates in Fig. 1. Let us
consider example 14 by Mueller (2014), which reasons about the turning on and
off of a light switch:

$\begin{array}[]{ll}\mathit{Happens}(e,t)\ \
\equiv&(e=\mathit{TurnOn}\land\allowbreak t=2)\ \ \lor\allowbreak\\\
&(e=\mathit{TurnOff}\land\allowbreak t=4)\end{array}$

Assuming circumscription, we can write the axioms
$\mathit{Happens}(\mathit{TurnOn},2)$ and
$\mathit{Happens}(\mathit{TurnOff},4)$, instead of writing the previous
formula, while ensuring that there are no events (resp., effects) other than
those stated. I.e., we can prove that the light is off at $t=6$, because we
can prove the absence of an event turning the light on between $t=4$ and
$t=6$. If we need to add a new event (e.g.,
$\mathit{Happens}(\mathit{TurnOn},5)$) we only have to add it, instead of
modifying the formula that expresses the circumscription of the narrative. It
has to be noted that in this case the circumscribed formula is simple, but the
circumscription of more complex formulas is more involved.

Similarly, since EC assumes the circumscription of the rest of the predicates
defined in the narrative ($\mathit{InitiallyN}$, $\mathit{InitiallyP}$,
$\mathit{Initiates}$, $\mathit{Terminates}$, $\mathit{Releases}$, and
$\mathit{Trajectory}$), we have that the explicitly known effects of events
are the only effects of events.

EC does not assume circumscription for the underlying theory. Since BEC1 and
BEC2 are definitions which can be expanded wherever they appear, they do not
need to be taken care of specially.

However, for the rest of the BEC theory axioms in Fig. 2, from BEC3 to BEC7,
we cannot apply this assumption because they are not circumscribed and they
are implications: $\mathit{HoldsAt}$ is true _if_ the body of one of its
corresponding axioms holds. This means that, if we cannot infer that
$\mathit{HoldsAt}(f,t)$ is true, then, we cannot deduce that
$\lnot\mathit{HoldsAt}(f,t)$ is true. Instead, the falsehood of
$\mathit{HoldsAt}(t,f)$ must be inferred through the axioms BEC5 and BEC7 if
this is supported by direct evidences defined in the narrative. It is
important to note that if the narrative describes a scenario in which it is
possible to deduce that a fluent $f$ is true and false at the same point in
time $t$, this narrative is inconsistent and there are no valid models for
this scenario. Furthermore, if a given narrative is described in terms of the
truth or falsehood of a fluent $f$ at some point in time $t$, but we are not
able to decide this value, then there are multiple valid models because we
have that $\mathit{HoldsAt}(t,f)\lor\allowbreak\lnot\mathit{HoldsAt}(t,f)$.

Let us describe below how we use s(CASP) to compute the circumscription based
on predicate completion Mueller (2014); Lee and Palla (2012) while we are able
to express the truth/falsehood of $\mathit{HoldsAt}$ using classical negation.

###  3.2 Modeling BEC with s(CASP)

Two key factors contribute to s(CASP)’s ability to model Event Calculus: the
preservation of non-ground variables during the execution and the integration
with constraint solvers.

Treatment of variables in s(CASP): Thanks to the use of non-ground variables,
s(CASP) is able to directly model Event Calculus axioms that would otherwise
require ‘‘unsafe’’ rules (Section 2.1.5). Let us take, for example, rule BEC4
of Fig. 2. In a straightforward encoding (see Fig. 3), the parameter $t$ (T in
the code), which appears in the head and does not appear in a positive literal
in the body (i.e., it only appears in $\lnot\mathit{StoppedIn}(0,f,t)$) would
be classified as unsafe by a mainstream ASP system.

It may be argued that a way to overcome this issue would be to translate the
negation in the axioms as classical negation, i.e., -stoppedIn(0, F, T).
However, this would need to generate a negation of the two clauses of
stoppedIn/3 which would in turn need the (classical) negations of
terminates/3, happens/2, and releases/3. However, these narrative predicates
do not come with a definition stating when they are false, in the classical
sense of negation.

An ASP solver such as _clingo_ Gebser et al. (2014) will not be able to
directly process unsafe rules like this. The standard approach to fix unsafe
rules is to add a positive literal defining the domain of the unsafe variable
(T in this case), but this is not feasible if we want to maintain the property
that T represents time and is therefore not discrete and not finite. On the
other hand, the top-down execution strategy of s(CASP) makes it possible to
keep logical variables both during execution and in answer sets and therefore
free (logical) variables can be handled in heads and in negated atoms.

Integration with constraint solvers: The s(CASP) system has a generic
interface to enable plugging in constraint solvers. s(CASP) currently includes
the CLP($\mathbb{Q}$) linear constraints solver by Holzbaur (1995), that
supports the arithmetic constraints $<,>,=,\leq,\geq$. This is used to
implement the definitions and axioms of BEC that require comparisons of points
in (continuous) time and to solve the equations that arise from these
comparisons. The selection of CLP($\mathbb{Q}$) instead of the faster
CLP($\mathbb{R}$) is motivated by soundness reasons. Since CLP($\mathbb{R}$)
uses internally floating-point numbers, rounding and approximations compromise
accuracy and termination of some code. On the other hand, CLP($\mathbb{Q}$)
represents rational numbers exactly and therefore it should not introduce any
calculation error. One example in which the use of floating-point numbers
would be inadequate is the code in Fig. 5, which uses the factor $\frac{4}{3}$
and that does not have an exact floating-point representation.

The s(CASP) infrastructure is however parametric w.r.t. the underlying
constraint solver, and other implementations of constraint domains can be
implemented and plugged in if necessary. As an example, s(CASP) includes a
solver for disequality in the Herbrand domain (Sec. 2.1.3), which is necessary
to generate the dual of almost any interesting program.

⬇

1%% BEC1

2stoppedIn(T1,F,T2) :-

3 T1.<.T, T.<.T2,

4 terminates(E,F,T),

5 happens(E,T).

6

7stoppedIn(T1,F,T2) :-

8 T1.<.T, T.<.T2,

9 releases(E,F,T),

10 happens(E,T).

11

12%% BEC2

13startedIn(T1,F,T2) :-

14 T1.<.T, T.<.T2,

15 initiates(E,F,T),

16 happens(E,T).

17

18startedIn(T1,F,T2) :-

19 T1.<.T, T.<.T2,

20 releases(E,F,T),

21 happens(E,T).

22

23%% BEC3

24holdsAt(F2,T2) :-

25 initiates(E,F1,T1),

26 happens(E,T1),

27 trajectory(F1,T1,F2,T2),

28 not stoppedIn(T1,F1,T2).

29%% BEC4

30holdsAt(F,T) :-

31 0.<.T,

32 initiallyP(F),

33 not stoppedIn(0,F,T).

34

35%% BEC5

36-holdsAt(F,T) :-

37 0.<.T,

38 initiallyN(F),

39 not startedIn(0,F,T).

40

41%% BEC6

42holdsAt(F,T2) :-

43 T1.<.T2,

44 initiates(E,F,T1),

45 happens(E,T1),

46 not stoppedIn(T1,F,T2).

47

48%% BEC7

49-holdsAt(F,T2) :-

50 T1.<.T2,

51 terminates(E,F,T1),

52 happens(E,T1),

53 not startedIn(T1,F,T2).

54

55%% Consistency (automatically added)

56:- -holdsAt(F,T), holdsAt(F,T).

Figure 3: Basic Event Calculus (BEC) modeled in s(CASP)

###  3.3 Translating the BEC Axioms into s(CASP)

Our translation of the BEC axioms into s(CASP) is related to the translation
used by the systems EC2ASP and F2LP Lee and Palla (2012, 2020). We differ in
three aspects that improve performance for a top-down system, fully use
s(CASP)’s ability to treat unbound variables, and do not compromise the
soundness of the translation (according to the proofs presented by Lee and
Palla (2012)). These are: the treatment of rules with negated heads, the
possibility of generating unsafe rules, and the use of constraints over dense
domains (rationals, in our case). We describe below, with the help of a
running example, the translation that turns logic statements (as found in BEC)
into an s(CASP) program. The code corresponding to the translations of the
axioms of BEC in Fig. 2 can be found in Fig. 3. s(CASP) code follows the
syntactical conventions of logic programming: constants (including function
names) and predicate symbols start with a lowercase letter and variables start
with an uppercase letter. In addition, numerical constraints are written as
constraints in s(CASP), (e.g., .<.) to make it clear that they do not
correspond to Prolog’s arithmetic comparisons:

  * •

Atoms and Constants: Their names are preserved. _Uniqueness of Names_ Shanahan
(1999) is assumed by default (and enforced) in logic programming.

  * •

Constraints: Predicates that represent constraints (e.g., on time) are
directly translated to their counterparts in s(CASP). E.g., $t_{1}<t_{2}$
becomes T1 .<. T2, which is handled by the CLP($\mathbb{Q}$) solver. The
translation is parameterized on the constraint domain.

  * •

Definitions: The axiomatization of BEC uses definitions of the form
$D(x)\equiv\exists yB(x,y)$, where $B(x,y)$ is a conjunction of (possibly
negated) atoms, disjunctions of atoms, and constraints (e.g., BEC1). The use
of these definitions makes it easier to build and reuse conceptual blocks out
of basic predicates. They are however not strictly necessary _per se_ as
predicates. For performance reasons we treat them as if they were written as
$\forall x(D(x)\leftarrow\exists yB(x,y))$, following the work of Lee and
Palla (2020). Since $D$, as mentioned above, is given a name as a convenience
to write the BEC axioms, we can ignore its truth value in the (partial) models
that s(CASP) generates because if it were expanded where it is used, it would
have disappeared. Therefore, the models returned using implication or
equivalence for the definition of $D$ are the same.

  * •

Rules with Positive Heads: A rule (e.g., BEC6)

$\forall x(H(x)\leftarrow\exists y(A(y)\land\allowbreak\neg
B(x,y)\land\allowbreak x<y))$

where $x<y$ is a constraint, is translated into

⬇

1h(X) :- X.<.Y, a(Y), not b(X,Y).

The constraint X.<.Y could be placed anywhere in the clause. However, in top-
down evaluation schemes, the general recommendation is to execute constraints
as soon as possible to use a _constraint and generate_ mechanism instead of
_generate and test_ in order to improve performance. In the very common case
where user-level constraint operations are translated into constraint
propagation, which is usually required to be deterministic, executing them
earlier in the tree simplifies the constraints without performing internal
search or creating search branches. On the other hand, by constraining the
domains of the variables earlier, the size of the search trees needed by calls
to user predicates (a(Y), not b(X, Y) in this case) are reduced.

  * •

Rules with Negated Heads: BEC rules 5 and 7 infer negated heads
$\neg\mathit{HoldsAt}(f,t)$ while rules 4 and 6 infer positive heads
$\mathit{HoldsAt}(f,t)$, i.e., they follow, respectively, the scheme

$\forall x(\neg H(x)\leftarrow\exists yA(x,y))\ \ \land\allowbreak\ \ \forall
x(H(x)\leftarrow\exists yB(x,y))$

The standard approach to translate rules with negated heads is to convert them
into denials Lee and Palla (2012) such as :- a(X,Y), h(X). Our approach is to
create instead the atom -h(X) to denote (Section 2.1.1) the negation of h(X)
and a rule that captures the explicit evidence that h(X) is false:

⬇

1-h(X) :- a(X,Y).

This makes it possible to invoke -h(X) as a regular predicate in a top-down
execution. The compiler will additionally (Section 2.1.1) generate denials to
ensure that -h(X) and h(X) cannot be simultaneously true. Therefore, s(CASP)
will detect an inconsistency if both $\mathit{HoldsAt}(f,t)$ and
$\neg\mathit{HoldsAt}(f,t)$ can be simultaneously derived from the narrative.
Having rules stating explicitly when $\neg\mathit{HoldsAt}(f,t)$ can be
derived makes it possible to query for it, as some BEC rules need. We will
later see how this is connected with the translation of the narrative.

  * •

Rules with Disjunctive Bodies: A rule (e.g., BEC1)

$\forall x[H(x)\leftarrow\exists y(\ (A(x,y)\lor\allowbreak
B(x,y))\land\allowbreak C(x,y)\ )]$

is translated into two separate clauses:

⬇

1h(X) :- a(X,Y), c(X,Y).

2h(X) :- b(X,Y), c(X,Y).

###  3.4 Translation of the Narrative

Every basic BEC predicate $P(x)$ from the narrative (Fig. 1) is translated
into s(CASP) as a set of rules of the form

$P(x)\leftarrow\gamma$

where the body $\gamma$ is a conjunction of atoms, negated atoms, and
constraints that can be trivially $true$ in some cases. The rules
corresponding to the same $P(x)$ are assumed to state all the cases where
$P(x)$ is true.

Throughout this section we will use the light scenario problem from Mueller
(2014, example 14): a two-color bulb lamp can be switched on and off. We want
to be able to answer when the light is on (and its color in this case) and
off. We will present the BEC narrative and its translation into s(CASP),
available in full in Figure 4.

⬇

1happens(turn_on, 2).

2happens(turn_off, 4).

3happens(turn_on, 5).

4

5initiates(turn_on, on, T).

6

7terminates(turn_off, on, T).

8terminates(turn_off, red, T).

9terminates(turn_off, green, T).

10trajectory(on, T1, red, T2) :-

11 T1.<.T2,

12 T2.<.T1+1.

13trajectory(on, T1, green, T2) :-

14 T2.>=.T1+1.

15

16releases(turn_on, red, T).

17releases(turn_on, green, T).

Figure 4: Narrative of the light scenario modeled in s(CASP)

##### Events:

Let us consider the description below:

$\begin{array}[]{ll}\mathit{Happens}(e,t)\ \
\equiv&(e=\mathit{TurnOn}\land\allowbreak(t=2\lor\allowbreak t=5))\ \
\lor\allowbreak\\\ &(e=\mathit{TurnOff}\land\allowbreak t=4)\end{array}$

It states that the $\mathit{TurnOn}$ event will happen at time $t=2$ and
$t=5$, and that $\mathit{TurnOff}$ will happen at $t=4$. As we mentioned
before, since EC assumes circumscription, it is equivalent to the axioms
$\mathit{Happens}(\mathit{TurnOn},2)$, $\mathit{Happens}(\mathit{TurnOff},4)$
and $\mathit{Happens}(\mathit{TurnOn},5)$, which are translated as facts
(lines 1-3 of Fig. 4).

##### Event Effects:

The effects of events are represented using the predicates $Initiates(e,f,t)$
and $Terminates(e,f,t)$. In our example, when the event $\mathit{TurnOn}$
happens, the light is put in $on$ status; similarly, when the event
$\mathit{TurnOff}$ happens, the light will not be $on$, $red$ or $green$:

$\begin{array}[]{lll}\mathit{Initiates}(e,f,t)&\equiv&(e=\mathit{TurnOn}\land\allowbreak
f=\mathit{On})\\\
\mathit{Terminates}(e,f,t)&\equiv&(e=\mathit{TurnOff}\land\allowbreak(f=\mathit{On}\lor\allowbreak
f=\mathit{Red}\lor\allowbreak f=\mathit{Green}))\end{array}$

In both cases, this can happen at any time $t$, and the translation again
becomes facts (lines 5-9 in Fig. 4)

##### Release from Inertia:

When turned on, the light emits red light for one second and after that it
starts to emit green light. $Trajectory$ expresses how this change depends on
the time elapsed since an event occurrence.

$\begin{array}[]{lll}\mathit{Trajectory}(s,t_{1},c,t_{2})&\equiv&(s=\mathit{On}\land\allowbreak
c=\mathit{Red}\land\allowbreak t_{1}<t_{2}\land\allowbreak
t_{2}<t_{1}+1)\;\lor\allowbreak\\\ &&(s=\mathit{On}\land\allowbreak
c=\mathit{Green}\land\allowbreak t_{2}\geq t_{1}+1)\end{array}$

The translation is in lines 10-14 of Fig. 4. $\mathit{Releases}$ states that
the color of the light is released from the commonsense law of inertia. After
a fluent is released, its truth value is not determined by BEC and it can
change. Thus, there may be models in which the fluent is true, and models in
which the fluent is false:

$\begin{array}[]{lll}\mathit{Releases}(e,f,t)&\equiv&(e=\mathit{TurnOn}\land\allowbreak(f=\mathit{Red}\lor\allowbreak
f=\mathit{Green}))\end{array}$

Note that the time parameter $t$ appears only in the head (it is universally
quantified). Releasing a fluent (lines 16 and 17 in Fig. 4) frees it up so
that other axioms in the domain description can be used to determine its truth
value, thus allowing us to represent continuous change of the fluent.

##### State Constraints:

State constraints usually contain $\mathit{HoldsAt}(f,t)$ or
$\lnot\mathit{HoldsAt}(f,t)$ and represent restrictions on the models. In our
running example, a light cannot be red and green at the same time:

$\begin{array}[]{l}\lnot\mathit{HoldsAt}(\mathit{Red},t)\lor\allowbreak\lnot\mathit{HoldsAt}(\mathit{Green},t)\end{array}$

Note that this is logically equivalent to $\forall t\
\lnot(\mathit{HoldsAt}(\mathit{Red},t)\land\allowbreak\mathit{HoldsAt}(Green,t))$
and is translated as :-holdsAt(red,T),holdsAt(green,T). Adding this denial to
the program in Fig. 4 does not change its models. However, if we change the
trajectory definition for the red light stating $t_{2}\leq t_{1}+1$ instead of
$t_{2}<t_{1}+1$ the state constraint is violated at $t_{2}=t_{1}+1$ and
therefore, there are no valid models.

##### A Note on Using $\neg\mathit{HoldsAt}(f,t)$ in the Narrative:

The narrative predicates may depend on what the BEC theory can deduce. In
other words, $\mathit{HoldsAt}(f,t)$ or $\neg\mathit{HoldsAt}(f,t)$ can
(perhaps indirectly) be used in the body $\gamma$ of a narrative rule (see an
example in Fig. 5). $\mathit{HoldsAt}(f,t)$ can be invoked directly, but
$\neg\mathit{HoldsAt}(f,t)$ ought to be called using classical negation, e.g.,
-holdsAt(F,T). As we mentioned before, the reason is that circumscription is
not applied to the EC axioms and we can deduce only the truth (or falsehood)
of $\mathit{HoldsAt}$ when we have direct evidence of either of them --- i.e.,
what the positive (holdsAt(F,T)) and negative (-holdsAt(F,T)) heads provide.

As we mentioned before, the consistency rule (line 56 in Fig. 3) introduced by
the compiler of s(CASP) would ensure that holdsAt(F,T) and -holdsAt(F,T) are
mutually exclusive by flagging an inconsistency. Note that if not holdsAt(F,T)
succeeds, then holdsAt(F,T) is false but it does not imply that -holdsAt(F,T)
is true (i.e., -holdsAt(F,T) $\Rightarrow$ not holdsAt(F,T), but it is not the
case that not holdsAt(F,T) $\Rightarrow$ -holdsAt(F,T)). Symmetrically for not
-holdsAt(F,T) we have that holdsAt(F,T) $\Rightarrow$ not -holdsAt(F,T).

In previous implementations of EC, such as F2LP, reasoning about the falsehood
of $\mathit{HoldsAt}(f,t)$ can be made using only the default negation,
implemented as negation as failure (i.e., not/1). Therefore, the presence of
classical negation in s(CASP) not only increases the expressive power from the
point of view of the programmer (by, e.g., determining whether a fluent is or
not active at some point in time), but it also ensures correctness in those
cases where -holdsAt(F,T) $\not\equiv$ not holdsAt(F,T), as inconsistent
models are discarded.

###  3.5 Continuous Change: A Complete Encoding

⬇

1#include bec_theory.

2

3max_level(10) :- not max_level(16).

4max_level(16) :- not max_level(10).

5

6initiallyP(level(0)).

7

8happens(overflow,T).

9happens(tapOn,5).

10

11initiates(tapOn,filling,T).

12terminates(tapOff,filling,T).

13initiates(overflow,spilling,T):-

14 max_level(Max),

15 holdsAt(level(Max), T).

16

17releases(tapOn,level(0),T):-

18 happens(tapOn,T).

19trajectory(filling,T1,level(X2),T2):-

20 T1.<.T2,

21 X2.=.X+4/3*(T2-T1),

22 max_level(Max),

23 X2.=<.Max,

24 holdsAt(level(X),T1).

25trajectory(filling,T1,overlimit,T2):-

26 T1.<.T2,

27 X2.=.X+4/3*(T2-T1),

28 max_level(Max),

29 X2.>.Max,

30 holdsAt(level(X),T1).

31

32trajectory(spilling,T1,leak(X),T2):-

33 holdsAt(filling, T2),

34 T1.<.T2,

35 X.=.4/3*(T2-T1).

Figure 5: Encoding of an Event Calculus narrative with continuous change

We consider now an extension of the water tap example by Shanahan (1999),
where we define two possible worlds and added a triggered fluent to describe
the ability of s(CASP) to model complex scenarios. In this example, a water
tap fills a vessel, whose capacity is either 10 or 16 units, and when the
level of water reaches the bucket rim, it starts spilling. Let us present the
main ideas behind its encoding, available in Fig. 5.

##### Continuous Change:

The fluent $\mathit{Level}(x)$ represents that the water is at level $x$ in
the vessel. The first $Trajectory$ formula (lines 19-24) determines the time-
dependent value of the $\mathit{Level}(x)$ fluent, which is active as long as
the $Filling$ fluent is true and the rim of the vessel is not reached. The
second $Trajectory$ formula (lines 25-30) allows us to capture the fact that
the water reached the rim of the vessel and overflowed. Note the $\frac{3}{4}$
factor that relates time and water amount. As mentioned before, if the
underlying solver approximates the numerical operations, water levels could be
miscalculated and therefore the answers to some queries could be wrong. The
use of CLP($\mathbb{Q}$) prevents this.

##### Uniqueness of $\mathit{Level}(x)$

A relevant question is whether the fluent $\mathit{Level}(x)$ could take two
different values at the same time. Intuitively, it should not, because if we
are modeling faithfully a physical system evolving under a series of events,
the level should be unique at any point in time. Note, however, that if this
were to happen, it would be because the narrative does not correspond to the
reality. The specification given by Shanahan (1999) includes explicitly an
axiom

$\mathit{HoldsAt}(\mathit{Level}(x_{1}),t)\land\allowbreak\mathit{HoldsAt}(\mathit{Level}(x_{2}),t)\rightarrow
x_{1}=x_{2}$

to avoid this situation.

We did not include it for two reasons: on the one hand, a careful inspection
of the narrative reveals that this could not be the case. On the other hand,
if this axiom were necessary, the model without it would allow the
simultaneous existence of two alternative water levels. That raises the
question whether the model is correct, as the narrative would in that case
allow two different, diverging events happen at the same time, or the
trajectories would allow two inconsistent fluents overlap. Just stating this
inconsistency is of little value in practice, as it does not help catch errors
in the model and it removes possible correct states.777Let us note that EC
does not preclude a fluent to have different associated values simultaneously:
it is only the semantics of this fluent that may disallow it. As an example,
let us take the fluent $\mathit{Occupied}(n)$ that expresses that the seat $n$
in a theater is occupied. Obviously, several instances for different $n$ can
be true at the same time.

##### Triggered Fluent:

The fluent $Spilling$ is triggered (lines 13-15) when the water level reaches
the rim of the vessel. As a consequence, the $Trajectory$ formula in lines
32-35 starts the fluent $Leak(x)$ and captures the amount of water leaked
while the fluent $Spilling$ holds.

##### Alternative Worlds:

As we mentioned in Section 2.1.4, the presence of even loops generates
different worlds. In our implementation, the clauses in lines 3-4 force the
vessel capacity to be either 10 or 16, and therefore, they create two possible
worlds/models: {max_level(10), not max_level(16),$\dots$} and {max_level(16),
not max_level(10),$\dots$}.

Different worlds can be used to model alternative scenarios where an event may
happen in one world and not in another. For this, a keyword #abducible is
provided as a shortcut in s(CASP). We will use it in Sec. 4.2, below.

##  4 Examples and Evaluation

The benchmarks used in this section are available at
http://www.cliplab.org/papers/EC-sCASP-TPLP2020/. They were run on a macOS
10.15.7 laptop with an Intel Core i5 at 2GHz.

###  4.1 Deduction

Deduction determines whether a state of the world is possible given a theory
and an initial narrative. We can perform deduction in BEC for the previous
examples through queries to the corresponding s(CASP) program. For the
_lights_ scenario (Fig. 4):

?-holdsAt(on,3) succeeds: it states that the light is on at time 3.

?--holdsAt(on,4.5) succeeds: the light is not on at time 4.5.888The decimal
number 4.5 is automatically converted to rational representation.

?-holdsAt(F,3) is true in one stable model containing holdsAt(green,3) and
holdsAt(on,3), meaning that the light is on and green at time 3.

Additionally, as we mentioned in Section 3.4, using the default negation not/1
we can check the absence of a proof for holdsAt/2 and -holdsAt/2. However,
there are time points, e.g., at time 1, where neither the truth nor the
falsehood for the fluent representing that the light is on can be deduced from
the program. Therefore, the queries ?- not holdsAt(on,1) and ?- not
-holdsAt(on,1) would both succeed.

Finally, let us use the water level scenario (Fig. 5) to make queries
involving time and the water level (that are continuous physical quantities):

?-holdsAt(level(H),15/2) is true when H=10/3.

?-holdsAt(level(10/3),T) is true when T=15/2.

Note that, as explained with more detail in the _Evaluation_ subsection below,
s(CASP) can operate and answer correctly queries involving rationals (and, in
general, dense domains as long as they are supported by the underlying
constraint solver) without having to modify the original program to introduce
domains for the relevant variables or to _scale_ the constants to convert
rationals into integers.

###  4.2 Abduction

Abductive reasoning can be used to determine a sequence of events/actions that
reaches a given state. In the case of ASP, actions are naturally captured as
the set of atoms that are true in a model that includes the initial and final
states, and that are consistent with the BEC theory. For the water scenario
(Fig. 5), let us assume we want to determine whether the water can reach a
level of 12 at time 14. The query ?-holdsAt(level(12),14) will return a single
model with a vessel size of 16 and the rest of the atoms in the model
capturing what must (not) happen to reach this state. For EC, the relevant
atoms are those related to the events that happen (as these trigger fluents
according to the model rules in initiates/3, releases/3, and trajectory/4)
and, to keep track of the state of the system, the atom holdsAt/2 and its
classical negation. If, for the query mentioned above, we restrict the model
to these atoms,999This can be done automatically by placing #show directives
in the source code. we obtain the following filtered model:

⬇

{ initiallyP(level(0)), not happens(tapOn,D | {D #> 0,D #< 5}),

holdsAt(level(0),5), happens(tapOn,5),

not happens(tapOff,F | {F #> 5,F #< 14}), holdsAt(level(12),14) }

where we have listed the atoms in increasing order of time stamp.

This subset of the model states what must happen to reach a state with a water level of 12 at time $t=14$. It captures events that must be observed (e.g., happens(tapOn,5), meaning that the water tap has to open at time $t=5$), what is the observable state of the fluents (holdsAt(level(12),14), meaning that the water level at $t=14$ is 12), but also what events must not happen (not happens(tapOn, D | {D #> 0,D #< 5}), meaning that the tap must not be opened between $t=0$ and $t=5$, or not happens(tapOff,F | {F #> 5,F #< 14}), meaning that the water tap must not be closed between $t=5$ and $t=14$).

Additionally, since s(CASP) only generates partial models, it does not contain
atoms that express actions that are not necessary for the conclusion, i.e.,
the plan does not contain references to actions (either positive or negative)
that do not interfere with the final state. For example, it does not state
that the event of closing the tap must or must not happen between $t=0$ and
$t=5$: whether this event happens or not is immaterial for the final result.
Other abductive tasks can be performed: adding the directive #abducible to the
fact happens(tapOn,5), we specify that it is possible (but not necessary) for
the tap to be open at time 5. As we mentioned in Section 3.5, this directive
is translated into code that creates different worlds/models. For the previous
query, ?-holdsAt(level(L),14) (that determines the level of water at $t=14$),
we obtain two alternative partial models:

  * •

One containing the literal happens(tapOn,5) meaning that the tap is open at
$t=5$, and therefore, the resulting model is the previous one.

  * •

Another one containing { holdsAt(level(0),14), initiallyP(level(0)), not happens(tapOn,G ${G#>0,G#<5}),nothappens(tapOn,5),nothappens(tapOn,E$|${E#>5,E#<14})$ | meaning that the tap is not open at $t=5$ (and neither for $0<t<5$, nor for $5<t<14$), and therefore, the water level at $t=14$ remains equal to 0, which causes the literal holdsAt(level(0),14) be part of the model.

Note that s(CASP) determined the truth value of $Happens$ and, more
importantly, performed constraint solving to infer the time ranges during
which some events ought (and ought not) to take place, represented by the
negated atoms in the models inferred by constructive negation. Since all
relevant atoms have a time parameter, they actually represent a _timed plan_.
Due to the expressiveness of constraints, this plan contains information on
time points when events must (not) happen and also on time _windows_
(sometimes in relation with other events) during which events must (not) take
place. Note that it would be impossible to (finitely) represent this interval
with ground atoms, as it corresponds to an infinite number of points.

###  4.3 Evaluation

A direct performance comparison of our implementation of BEC in s(CASP) with
implementations in other systems may not be meaningful: most previous systems
implement _discrete_ Event Calculus (DEC) and they do not support continuous
quantities. Since offering this support is one of the key points of our
proposal, giving up on it and comparing with an implementation DEC in s(CASP)
is pointless and defeats the main purpose of this piece of work. We will then
have to compare BEC in s(CASP) with how a system that implements DEC can be
used to approximate the results we can give.

One of the ASP-based tools that support DEC is F2LP, an ASP-based system that
according to Lee and Palla (2012) _‘‘outperforms _DEC reasoner_ Mueller
(2008b)’’_, reported there as the more efficient SAT-based implementation.
F2LP is a tool that executes DEC by turning first-order formulas under the
stable model semantics into a logic program without constraints that is then
evaluated using an ASP solver.

Our first evaluation compares the light scenario in Fig. 4 running under
s(CASP) with the F2LP translation under _clingo 5.1.1_ , the current version
of the state-of-the-art ASP system. Since the directive #domain is no longer
available in _clingo_ , we adapted the translation of F2LP adding
timestep(1..10) and timestep/1 to make the clauses safe (Appendix A of the
supplementary material accompanying the paper at the TPLP archive). While
under s(CASP) we can reason about time points in an unbounded, dense domain,
the encoding used by F2LP makes time belong to the integers (in particular, to
the interval from 1 to 10, with the previous timestep/1 fact). Therefore,
since the light can be red for $t>2,t<3$ and for $t>5,t<6$,101010When turned
on (at $t=2$ and $t=5$), the light emits red light for one second (see Section
3.4). there are no integer time points between 1 and 10 where the emitted
light is red. Therefore, the query ?-holdsAt(red,T) does not return any model
under _clingo_ , while the execution of the same query under s(CASP) returns
the constraint conjunctions T.>.2, T.<.3 and T.>.5, T.<.6.

In order to determine at what time point the red light is on using _clingo_ ,
we modified the program generated by F2LP to refine the timestep domain with
timestep(1..10*P):- precision(P), where the new predicate precision(P) makes
it possible to have a finer grain for the possible values of timestep by
increasing the value of P. With this modification, it is possible to check if
the light is red at time $t=5.9$ with _clingo_ by stating that we want a
precision of tenths (using precision(10)) and modifying the queries
accordingly, e.g., using ?-holdsAt(red,59). Similarly, using p=100 in
precision(P) it is possible to check for $t=5.99$ by querying
?-holdsAt(red,599), and so on.

This change (see Appendix B of the supplementary material accompanying the
paper at the TPLP archive, for the complete program) is in principle not
difficult to perform, but it undoubtedly obfuscates the resulting program (and
for more complex narratives it would be harder, impractical, or even
infeasible), and also impacts negatively its performance. Table 1(a) shows how
the additional precision necessary in the F2LP encoding increases the
execution run-time of _clingo_ by orders of magnitude. On the other hand,
s(CASP) does not have to adapt its encoding/queries and its performance does
not change.

Table 1: Comparative table of s(CASP) and F2LP+clingo.

(a) Run time (ms) comparison for the light scenario. Queries |  s(CASP) |  |  F2LP+clingo and precision
---|---|---|---
?-holdsAt(red,5.9) | 228 |  | 82 |  10
?-holdsAt(red,5.99) | 240 |  | 8,364 |  100
?-holdsAt(red,5.999) | 226 |  |  $>$ 5 min. | 1000

(b) Run time (ms) comparison for the water tap scenario.

Queries |  s(CASP) |  |  F2LP+clingo and precision
---|---|---|---
?-holdsAt(level(11),T) | 301 |  | 475 |  10*
|  |  | 77,305 | 100

(*) With this precision the value returned by _clingo_ is wrong.

The second benchmark is the water level scenario in Fig. 5. The physical model
needs continuous quantities but, as it happened in the previous case, its
execution with _clingo_ forces the level of water to be expressed using
integers. For example, the query ?-holdsAt(level(11),T) returns the value
T=53/4 (= 13.25) using s(CASP),111111s(CASP) returns a rational number because
it uses the rational constraint solver CLP($\mathbb{Q}$) in order not to lose
precision, as would happen if using floating-point numbers. s(CASP) can
however output them in decimal notation by using the command-line flag -r.
while the execution under _clingo_ fails: the level of water is
$h=10.\overline{6}$ at time $t=13$ and $h=12$ at time $t=14$; therefore there
is no integer point in time $t$ with a level of water $h=11$.

As before, we modified the program generated by F2LP by adding the predicate
precision(P) to specify the precision of the program by scaling the numbers
_clingo_ deals with, which is necessary to determine at what time the level of
the water is $11$. For this example, the resulting encoding (see Appendix C of
the supplementary material accompanying the paper at the TPLP archive) is more
complex than for the previous benchmark. Additionally, this example shows that
the scaling value depends on the particular benchmark: precision(10) is not
fine-grained enough to capture the solution, and we have to go up to
precision(100) to obtain a model with T=1325 (corresponding to $t=13.25$, the
correct value) for the query holdsAt(level(1100),T).

An undesirable effect of rounding in ASP is that rounding may not only make
programs fail, but it may make them succeed with wrong answers. For example,
in the water level example, with precision(10), the query
holdsAt(level(110),T) holds with T=133 (which would correspond to $t=13.3$).
This value is not right, and it is due to arithmetic rounding performed during
the program execution.

Also, note that increasing P as powers of 10, as we have done, may not always
work: scaling units to make an answer such as 1/3 expressible as integers
needs the scaling factor of 3 included. That points to the need to have some
knowledge about the program answers _before_ scaling the program, or to
transform the whole program by using multipliers containing e.g. all the
denominators that can appear at run-time during the program execution.

Table 1(b) shows that, also for this benchmark, the additional precision
increases the execution run-time of _clingo_ by orders of magnitude.

##  5 Related Work

Previous work translated _discrete_ EC into ASP by reformulating the EC models
as first-order stable models and translating the (almost universal) formulas
of EC into a logic program that preserves stable models. Given a finite
domain, EC2ASP (and its evolution, F2LP) compiles (discrete) Event Calculus
formulas into ASP programs Lee and Palla (2020, 2012). This translation scheme
relies on two facts: the semantics of second-order circumscription and first-
order stable models coincide on canonical formulas, and almost-universal
formulas can be transformed into a logic program while preserving the stable
models. As a result, computing models of Event Calculus descriptions can be
done by computing the stable models of an appropriately generated program.

Clearly, approaches featuring discrete domains cannot faithfully handle
continuous quantities such as time. In addition, because of their reliance on
SAT solvers to find the stable models, they can only handle safe programs. In
contrast, in the s(CASP) system, because of its direct support for predicates
with arbitrary terms, constructive negation, and the novel forall mechanism
Marple et al. (2017); Arias et al. (2018), program safety is not a
requirement. Thus, s(CASP) can model Event Calculus axioms much more directly,
elegantly, and in continuous domains.

The approaches mentioned above assume discrete quantities and do not support
reasoning about continuous time or change. As long as SAT-based ASP systems
are used to model Event Calculus, continuous fluents cannot be
straightforwardly expressed since they require unbound or dense domains for
the variables. The work closest to incorporating continuous time makes use of
SMT solvers. In this approach, constraints are incorporated into ASP and the
grounded theory is executed using an SMT solver, as in Lee and Meng (2013).
However, this approach has not been directly applied to modeling the Event
Calculus. The closest tool chain is ASP Modulo Theory to SAT Modulo Theory
(ASPMT2SMT) by Bartholomew and Lee (2014) that uses _gringo_ to partially
ground the ASPMT theories and generate constraints that are processed by _Z3_
de Moura and Bjørner (2008). However, regular, discrete ASP variables are at
the heart of the model, and these are grounded and used to generate the
constraints. Therefore, if these discrete variables approximate continuous
variables in the model, the constraints generated will only approximate the
conditions of the original problem and therefore their solutions will also be
an approximation (or a subset) of the solutions for the real problem. In other
words, the initial discretization done for the ASP variables will be
propagated via the generated constraints to the final solutions that will, in
the best case, be a discretized version of the actual solutions. As an
example, if time is discretized, the solutions to the model will suffer from
this discretization.

EC can be written as a (Horn-clause) logic program, but it cannot be executed
directly by Prolog, as reported by Shanahan (2000), because it lacks some
necessary features, such as constructive negation, deduction of negated atoms,
and (to some extent) detection of infinite failure. The last one can to some
degree be worked around by using variants of Prolog implementations that
feature loop-breaking mechanisms in the presence of constraints, as done by
Arias and Carro (2019). The other points may eventually need ad-hoc coding for
every example or crafting an interpreter able carry out deduction tailored to
the task.

A common approach is to write a metainterpreter specific to the EC variant at
hand. This can be as complex as writing a (specialized) theorem prover or,
more often, a specialized interpreter whose correctness is difficult to
ascertain (see the code by Chittaro and Montanari (1996)). Therefore, some
Prolog implementations of EC do not completely formalize the calculus or
implement a weaker version. In our case, we leverage the capabilities of
s(CASP) to provide constructive, sound negation, negative rule heads, and loop
detection.

##  6 Conclusions

We showed how Event Calculus can be modeled in s(CASP), a goal-directed
implementation of constraint answer set programming with predicates, with
fewer limitations than other approaches. s(CASP) can capture the notion of
continuous time (and, in general, fluents) in Event Calculus thanks to its
grounding-free top-down evaluation strategy. It can also represent complex
models and answer queries in a flexible manner thanks to the use of
constraints.

The main contribution of the paper is to show how Event Calculus can be
directly modeled using s(CASP), an ASP system that seamlessly supports
constraints. The modeling of Event Calculus using s(CASP) is more elegant and
faithful to the original axioms compared to other approaches such as F2LP,
where time has to be discretized. While other approaches such as ASPMT do
support continuous domains, their reliance on SMT solvers makes constraints
and dependencies among variables be lost during grounding. The use of s(CASP)
brings other advantages: for example, in a query-driven system the trace of
the proof / generation of the model is a justification for the answers to a
query. Likewise, explanations for observations via abduction are also
generated for free, thanks to the goal-directed, top-down execution of
s(CASP).

To the best of the authors’ knowledge, our approach is the only one that
faithfully models continuous-time Event Calculus under the stable model
semantics. All other approaches discretize time and thus do not model EC in a
sound manner. Our approach supports both deduction and abduction with little
or no additional effort.

The work reported in this paper can be seen as one of the first non-trivial
applications of s(CASP). It illustrates the advantages that goal-directed ASP
systems have over grounding and SAT solver-based ones for certain domains /
classes of applications. The Event Calculus and its realization through
s(CASP) is being used to model real-world avionics systems in the aerospace
industry Hall et al. (2021). Avionics systems are cyber-physical system
consisting of sensors and actuators. Sensors are modeled as fluents while
actuator actions correspond to events. The goal is to use the s(CASP) EC model
to verify (timed) properties of these avionics systems as well as to identify
gaps with respect to system requirements. Abductive capabilities of s(CASP)
are being used to troubleshoot the system as well as to find gaps in system
design. The overarching goal of the project is to build event-calculus based
tools for avionics software systems assurance.

##### Competing interests:

The author(s) declare none.

## References

    * Arias and Carro (2019) Arias, J. and Carro, M. 2019\.  Description, Implementation, and Evaluation of a Generic Design for Tabled CLP.  Theory and Practice of Logic Programming 19, 3 (May), 412--448.
    * Arias et al. (2018) Arias, J., Carro, M., Salazar, E., Marple, K., and Gupta, G. 2018\.  Constraint Answer Set Programming without Grounding.  Theory and Practice of Logic Programming 18, 3-4, 337--354.
    * Arias et al. (2019) Arias, J., Chen, Z., Carro, M., and Gupta, G. 2019\.  Modeling and Reasoning in Event Calculus Using Goal-Directed Constraint Answer Set Programming.  In Pre-Proc. of the 29th Int’l. Symposium on Logic-based Program Synthesis and Transformation.
    * Bartholomew and Lee (2014) Bartholomew, M. and Lee, J. 2014\.  System aspmt2smt: Computing ASPMT Theories by SMT Solvers.  In 14th European Conference on Logics in Artificial Intelligence. LNCS, vol. 8761. Springer, 529--542.
    * Chittaro and Montanari (1996) Chittaro, L. and Montanari, A. 1996\.  Efficient Temporal Reasoning in the Cached Event Calculus.  Computational Intelligence 12, 359--382.
    * Clark (1978) Clark, K. L. 1978\.  Negation as Failure.  In Logic and Data Bases, H. Gallaire and J. Minker, Eds. Springer, 293--322.
    * de Moura and Bjørner (2008) de Moura, L. M. and Bjørner, N. 2008\.  Z3: An Efficient SMT Solver.  In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, C. R. Ramakrishnan and J. Rehof, Eds. Lecture Notes in Computer Science, vol. 4963. Springer, 337--340.
    * Dovier et al. (2000) Dovier, A., Pontelli, E., and Rossi, G. 2000\.  A Necessary Condition for Constructive Negation in Constraint Logic Programming.  Information Processing Letters 74, 3-4, 147--156.
    * Erdem and Lifschitz (2003) Erdem, E. and Lifschitz, V. 2003\.  Tight Logic Programs.  Theory Pract. Log. Program. 3, 4-5, 499--518.
    * Ferraris et al. (2011) Ferraris, P., Lee, J., and Lifschitz, V. 2011\.  Stable Models and Circumscription.  Artificial Intelligence 175, 1, 236--263.
    * Gebser et al. (2014) Gebser, M., Kaminski, R., Kaufmann, B., and Schaub, T. 2014\.  Clingo = ASP + Control: Preliminary Report.  arXiv 1405.3694.
    * Gelfond and Lifschitz (1988) Gelfond, M. and Lifschitz, V. 1988\.  The Stable Model Semantics for Logic Programming.  In 5th International Conference on Logic Programming. 1070--1080.
    * Gupta et al. (2007) Gupta, G., Bansal, A., Min, R., Simon, L., and Mallya, A. 2007\.  Coinductive Logic Programming and its Applications.  In 23rd Int’l. Conference on Logic Programming. Springer, 27--44.
    * Hall et al. (2021) Hall, B., Varanasi, S. C., Fiedor, J., Arias, J., Basu, K., Li, F., Bhatt, D., Driscoll, K., Salazar, E., and Gupta, G. 2021\.  Knowledge-Assisted Reasoning of Model-Augmented System Requirements with Event Calculus and Goal-Directed Answer Set Programming.  In Proc. 8th Workshop on Horn Clause Verification and Synthesis.
    * Hermenegildo et al. (2012) Hermenegildo, M. V., Bueno, F., Carro, M., Lopez-Garcia, P., Mera, E., Morales, J., and Puebla, G. 2012\.  An Overview of Ciao and its Design Philosophy.  Theory and Practice of Logic Programming 12, 1--2 (January), 219--252.
    * Holzbaur (1995) Holzbaur, C. 1995\.  OFAI CLP(Q,R) Manual, Edition 1.3.3.  Tech. Rep. TR-95-09, Austrian Research Institute for Artificial Intelligence, Vienna.
    * Kowalski and Sergot (1989) Kowalski, R. and Sergot, M. 1989\.  A Logic-Based Calculus of Events.  In Foundations of knowledge base management. Springer, 23--55.
    * Lee and Meng (2013) Lee, J. and Meng, Y. 2013\.  Answer set programming modulo theories and reasoning about continuous changes.  In 23rd Int’l. Joint Conference on Artificial Intelligence. 990--996.
    * Lee and Palla (2012) Lee, J. and Palla, R. 2012\.  Reformulating the Situation Calculus and the Event Calculus in the General Theory of Stable Models and in Answer Set Programming.  Journal of Artificial Intelligence Research 43, 571--620.
    * Lee and Palla (2020) Lee, J. and Palla, R. 2020\.  F2LP: Computing Answer Sets of First Order Formulas.  https://github.com/azreasoners/F2LP.  Accessed on October, 2020.
    * Lifschitz (1985) Lifschitz, V. 1985\.  Computing Circumscription.  In Proceedings of the 9th International Joint Conference on Artificial Intelligence. Los Angeles, CA, USA, August 1985. 121--127.
    * Lifschitz (1999) Lifschitz, V. 1999\.  Action Languages, Answer Sets, and Planning.  Springer Berlin Heidelberg, 357--373.
    * Lifschitz et al. (2001) Lifschitz, V., Pearce, D., and Valverde, A. 2001\.  Strongly Equivalent Logic Programs.  ACM Trans. Comput. Log. 2, 4, 526--541.
    * Marek and Truszczynski (1999) Marek, V. W. and Truszczynski, M. 1999\.  Stable Models and an Alternative Logic Programming Paradigm.  In The Logic Programming Paradigm: a 25-Year Perspective. Springer-Verlag, 375--398.
    * Marple et al. (2012) Marple, K., Bansal, A., Min, R., and Gupta, G. 2012\.  Goal-Directed Execution of Answer Set Programs.  In Principles and Practice of Declarative Programming, PPDP’12, Leuven, Belgium - September 19 - 21, 2012, D. D. Schreye, G. Janssens, and A. King, Eds. ACM, 35--44.
    * Marple and Gupta (2014) Marple, K. and Gupta, G. 2014\.  Dynamic Consistency Checking in Goal-Directed Answer Set Programming.  Theory and Practice of Loging Programming 14, 4-5, 415--427.
    * Marple et al. (2017) Marple, K., Salazar, E., and Gupta, G. 2017\.  Computing Stable Models of Normal Logic Programs Without Grounding.  arXiv 1709.00501.
    * Marriott and Stuckey (1998) Marriott, K. and Stuckey, P. J. 1998\.  Programming with Constraints: an Introduction.  MIT Press.
    * Marriott et al. (2006) Marriott, K., Stuckey, P. J., and Wallace, M. 2006\.  Constraint Logic Programming.  In Foundations of Artificial Intelligence. Vol. 2. Elsevier, 409--452.
    * McCarthy (1980) McCarthy, J. 1980\.  Circumscription - A Form of Non-Monotonic Reasoning.  Artificial Intelligence 13, 1-2, 27--39.
    * Mellarkod et al. (2008a) Mellarkod, V. S., Gelfond, M., and Zhang, Y. 2008a.  Integrating Answer Set Programming and Constraint Logic Programming.  Annals of Mathematics and Artificial Intelligence 53, 1-4, 251--287.
    * Mellarkod et al. (2008b) Mellarkod, V. S., Gelfond, M., and Zhang, Y. 2008b.  Integrating Answer Set Programming and Constraint Logic Programming.  Tech. rep., Texas Tech University. October.  This is a long version of Mellarkod et al. (2008a), available at https://www.depts.ttu.edu/cs/research/documents/46.pdf.
    * Mueller (2008a) Mueller, E. T. 2008a.  Chapter 17: Event calculus.  In Handbook of Knowledge Representation, F. van Harmelen, V. Lifschitz, and B. Porter, Eds. Foundations of AI, vol. 3. Elsevier, 671 -- 708.
    * Mueller (2008b) Mueller, E. T. 2008b.  Discrete event calculus reasoner documentation.  Software documentation, IBM Thomas J. Watson Research Center, PO Box 704.  Available at: http://decreasoner.sourceforge.net/. Accessed on October, 2020.
    * Mueller (2014) Mueller, E. T. 2014\.  Commonsense reasoning: an event calculus based approach.  Morgan Kaufmann.
    * Shanahan (1999) Shanahan, M. 1999\.  The Event Calculus Explained.  In Artificial Intelligence Today. Springer, 409--430.
    * Shanahan (2000) Shanahan, M. 2000\.  An Abductive Event Calculus Planner.  The Journal of Logic Programming 44, 1-3, 207--240.
    * Stuckey (1991) Stuckey, P. 1991\.  Constructive negation for constraint logic programming.  In Proc. LICS’91. 328--339.