From TAMI

Contents 1 Intro 2 Extended EC: Relevant Considerations 3 Automated Theorem Proving 4 QR 5 CLP 6 ODE 7 Notes

Intro

There is no implementation for any form of reasoning (prediction, post-diction, planning, etc.) for Event Calculus with continuously varying parameters. We recently extended EC to specify independent component values of a cumulative effect individually which are summed implicitly. We want to implement a simulator that predicts evolution of a system of interacting processes for the extended EC formalism. Continuous change is described through relationships between parameters and derivatives, including (simultaneous) Ordinary Differential Equations (ODEs). Therefore, reasoning over First Order Logic (FOL) and ODEs and Algebraic Equations must be combined. As suggested in the literature in the past, Qualitative Reasoning methods may be of use as well. Here we investigate which techniques developed for Automated Theorem Proving, Qualitative Reasoning (QR), Constraint Logic Programming (CLP) and numerical reasoning can be combined to develop an efficient reasoning technique for reasoning about the extended EC.

Extended EC: Relevant Considerations

It has been suggested that QR techniques of discovering next landmark, where the continuous behavior governed by a set of DEs (and/or algebraic equations) changes, can be reused. Landmarks are often associated with actions, especially when those landmarks are associated with discontinuous changes in parameter values, for example any external interference such as force application. If the continuous behavior is altered, such as when a moving body comes to a stop as a result of opposing friction force, no action may be associated with landmarks. Friction force ceases to be in play, thereby changing equations governing continuous behavior of parameters such as acceleration, even though the value of function associated with corresponding friction parameter becomes constant zero (changing from a non-zero value before).

Necessary and/or sufficient conditions contain value comparisons such as Value(Vel(b₁), t) > Value(Vel(b₂), t). QR techniques employ (elementary) calculus theorems of intermediate value theorem, mean value theorem, etc. in qualitative analyses and they could be reused in quantitative analyses of mathematical conditions.

Effect of action or break in discontinuity happens just after the action, i.e. axiomatically there is a small delay in effects of actions. For example, fluent AHF becomes true after small time Δ (Limit⁺_{r → ∞} 1/r), by axiom (B5). i.e. NAHF is changed after Δ time that force has been applied, by axiom (B18). Therefore, conditions such as that of axiom (B11) are to be tested for time Δ after action happens. There has been some research in the CLP domain that accounts for such delays that could be reused. Axioms (B5), (B18) and (B11) from the multiple blocks axiom are presented below.

(B5) Initiates(ApplyHF(f, b, v), AHF(f, b, v), t)

(B18) HoldsAt(AHF(f, b, v), t) → PartValue(NAHF(b), t, ..., v)

(B11) HoldsAt(On(b1, b2), t) ∧ Value(Vel(b1), t) = Value(Vel(b2), t) ∧ HoldsAt(SR(b1, b2), t) 
     → Value(Fr(b1, b2), t) = -1 × Value(CKF(b1, b2), t) × Value(FbBA(b2, b1), t) 
         ∧ Value(Acc(b1), t) - Value(Acc(b2), t) > 0 ∧ ¬HoldsAt(SL(b1, b2), t)

Furthermore, CLP techniques will be of use when parameter relationships are described by algebraic equations, rather than ODEs, and in separating algebraic conditions (or constraints) from logic conditions.

Efficient ODE solving techniques are required to evaluate changes in parameter values described via differential equations.

EC uses a FOL-based representation which may be reformulated to a second order formula for default reasoning via circumscription. We will initially restrict to those cases where domain descriptions after inclusion of the default assumptions are a FO formula. While there are many automated theorem provers such as SNARK, and specialized EC reasoners such as F2LP, however choices are restricted after inclusion of aggregates. Besides, there are no EC reasoners for continuous change, although CLP has been used for process reasoning before [herrmann1996].^[1]

Languages such as Denotational Proof Languages (DPL) for expressing specialized proof-search algorithms (and formal proofs as well) could be used to speed up from generalized FOL theorem proving techniques.

Automated Theorem Proving

QR

CLP

ODE

Notes

1. ↑ Herrmann and Thielscher generalize concepts Trajectory and AntiTrajectory introduced by Shanahan. Continuous change cannot be described via ODEs, however.