A graph-based spatial temporal logic for knowledge representation and automated reasoning in cognitive robots

TL;DR

This paper introduces a graph-based spatial temporal logic designed for knowledge representation and reasoning in cognitive robots, balancing expressiveness and computational tractability, with a decidable satisfiability and a SAT-based deduction system.

Contribution

It presents a novel graph-based spatial temporal logic with a Hilbert style axiomatization, ensuring soundness, completeness, and practical implementability for robotic applications.

Findings

Decidable satisfiability of the proposed logic.

Sound and complete deduction system.

Implementation via SAT solver.

Abstract

We propose a new graph-based spatial temporal logic for knowledge representation and automated reasoning in this paper. The proposed logic achieves a balance between expressiveness and tractability in applications such as cognitive robots. The satisfiability of the proposed logic is decidable. We apply a Hilbert style axiomatization for the proposed graph-based spatial temporal logic, in which Modus ponens and IRR are the inference rules. We show that the corresponding deduction system is sound and complete and can be implemented through SAT.