A First-Order Semantics for Golog and ConGolog under a Second-Order Induction Axiom for Situations

ABSTRACT. Golog and ConGolog are languages defined in the situation calculus for cognitive robotics. Given a Golog program P, its semantics is defined by a macro Do(P,s,s') that expands to a logical sentence that captures the conditions under which performing P in s can terminate in s'. A similar macro is defined for ConGolog programs. In general, the logical sentences that these macros expand to are second-order, and in the case of ConGolog, may involve quantification over programs. In this paper, we show that by making use of the foundational axioms in the situation calculus, these macro expressions can actually be defined using first-order sentences.