Limbo – A Reasoning System for First-Order Limited Belief

First-order logic is a formal language that can express statements like "Frank is the father of Sally" (or "fatherOf(Sally) == Frank"), allows variables as in "x is the father of Sally" (or "fatherOf(Sally) == x") and statements about existence like "Sally has a father" (or "It exists an x such that x is the father of Sally" [or "∃ x . fatherOf(Sally) == x"]) as well as universality as in "Everyone has a father" (or "For all y there is an x such that x is the father of y" [or "∀ y ∃ x . fatherOf(x) == y"]).

Using a complex enough formula in first-order logic, you can express a large number of things. However, it is not possible to determine all consequences of a first-order statement. So even if you know that some first-order sentence is true, there might be some other sentence that you would have to think very long about to find out that it is implied by your existing knowledge, after which you can say that you know it, too. But beforehand, you had no idea.

To represent this observation that knowledge is limited by reasoning capability, this system uses explicit operators "Kk>" and "Mk>" for "Using k reasoning steps, I know that ..." or "Using k reasoning steps, I still consider it possible that ...". A reasoning step basically looks like "x could be Fred, and then ..., but x could also be Frank, and then ..., or x could be ...". Statements that are limited in the number of times this is done can be checked automatically.

An example given is: The only thing you know is that Sally's father is either Fred or Frank, and rich. Then it can be automatically proven that "K There is a person x who is Sally's father, and rich, and M x is not Sally's father".

This probably sounds like a strange thing to say. How can "x is Sally's father and M x is not Sally's father" ever be true? The important thing here is that reasoning steps for M and K always start from the known facts, so "M x is not Sally's father" is true for any x, because no matter how hard you think, you don't know who Sally's father is, so it's possible that it's not x.

In fact, the example is intended to express "I know that Sally's father is rich, but I don't know who he is."

That seems neat. I'll have to try and see if I can model my problem with that.

>Limbo is a programming language for writing distributed systems

Limbo was

I fixed it for you.

I thought the clarification to be self-evident, for what it's worth.