# Proof Theory of a Multi-Lane Spatial Logic

arXiv: https://arxiv.org/abs/1504.06986 · HTML: https://mlsanity.com/paper/1504.06986/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Apr 2015.

## Built on by (most cited first, 1 of 1)

- [Formalizing and Evaluating Requirements of Perception Systems for Automated Vehicles using Spatio-Temporal Perception Logic](https://mlsanity.com/paper/2206.14372/) (2022)

## Abstract (arXiv)

We extend the Multi-lane Spatial Logic MLSL, introduced in previous work for proving the safety (collision freedom) of traffic maneuvers on a multi-lane highway, by length measurement and dynamic modalities. We investigate the proof theory of this extension, called EMLSL. To this end, we prove the undecidability of EMLSL but nevertheless present a sound proof system which allows for reasoning about the safety of traffic situations. We illustrate the latter by giving a formal proof for the reservation lemma we could only prove informally before. Furthermore we prove a basic theorem showing that the length measurement is independent from the number of lanes on the highway.