Limbo: A reasoning system for limited belief

Abstract

We introduce LIMBO, a reasoning system for limited belief. The system features a highly expressive language with first-order quantification, functions and equality, sorts, and introspective belief modalities. Reasoning is based on clause subsumption, unit propagation, and case splits. Decidability and sometimes even tractability is achieved by limiting the number of case splits. This demo illustrates the practical utility of limited belief by way of toy examples as well as the games of Sudoku and Minesweeper.