Translating mission plans into logic for autonomous space robots

Autonomous robots operating on distant planets must reason about mission objectives and constraints without relying on human guidance or GPS. This work introduces the first benchmark for translating natural language mission documentation into First-Order Logic (FOL), using real NASA Planetary Data System records from 2003–2013 covering launch, cruise, and orbital phases. The authors manually annotated mission documents with FOL representations capturing temporal structure, agent roles, and operational dependencies, and provide predicate vocabularies to support controlled experiments with varying levels of prior knowledge. The dataset is released publicly and addresses a gap in research on converting high-level mission knowledge into machine-interpretable formal representations.