We focus on a rich axiomatization for actions in the situation calculus that includes, among other features, a solution to the frame problem for deterministic actions. Our work is foundational in nature, directed at simplifying the entailment problem for these axioms. Specifically, we make four contributions to the metatheory of situation calculus axiomatizations of dynamical systems: (1) We prove that the above-mentioned axiomatization for actions has a relative satisfiability property; the full axiomatization is satisfiable iff the axioms for the initial state are. (2)We define the concept of regression relative to these axioms, and prove a soundness and completeness theorem for a regression-based approach to the entailment problem for a wide class of queries. (3) Our formalization of the situation calculus requires certain foundational axioms specifying the domain of situations. These include an induction axiom, whose presence complicates human and automated reasoning in the situation calculus. We characterize various classes of sentences whose proofs do not require induction, and in some cases, some of the other foundational axioms. (4)We prove that the logic programming language GOLOG never requires any of the foundational axioms for the evaluation of programs.

Cloud removal is a relevant topic in Remote Sensing, fostering medium- and high-resolution optical image usability for Earth monitoring and study. Recent applications of deep generative models and sequence-to-sequence-based models have proved their capability to advance the field significantly. Nevertheless, there are still some gaps: the amount of cloud coverage, the landscape temporal changes, and the density and thickness of clouds need further investigation. We fill some of these gaps in this work by introducing an innovative deep model. The proposed model is multi-modal, relying on both spatial and temporal sources of information to restore the whole optical scene of interest. We use the outcomes of both temporal-sequence blending and direct translation from Synthetic Aperture Radar (SAR) to optical images to obtain a pixel-wise restoration of the whole scene. The reconstructed images preserve scene details without resorting to a considerable portion of a clean image. Our approach’s advantage is demonstrated across various atmospheric conditions tested on different datasets. Quantitative and qualitative results prove that the proposed method obtains cloud-free images coping with landscape changes.