Limbo – A Reasoning System for First-Order Limited Belief
github.com
github.com
[1] http://www.let.rug.nl/festschriftnerbonne/08.%20Brouwer%20et...
On the bottom links under 'Tools' there are some related systems as well.
http://cplint.lamping.unife.it/example/examples.swinb http://cplint.lamping.unife.it/example/inference/inference_e...
The github repository of cplint is:
The first and obvious answer is that "this is software running on hardware, as apposed to being biologically-based".
It might sound like I'm being facetious but your question is really that broad.
Nice try, Bezos!
Here at Amazon, we care about the little things like that because we have to. For now. Again, thanks for helping us get one step closer to not having to.
EDIT: Save those downvotes for when posts are incapable of contributing at all. Jokes you don't find funny don't count. I laughed at the parent post, so it contributed to my enjoyment.
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 "K<k>" and "M<k>" 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<1> There is a person x who is Sally's father, and rich, and M<1> x is not Sally's father".
This probably sounds like a strange thing to say. How can "x is Sally's father and M<1> 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<1> 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."
Would suggest "There is already a software project called Limbo, although it's in a quite different domain." In fact there is already also this: https://sourceforge.net/projects/limbopcemulator/ and the Limbo language is almost definitely not in serious use anywhere. (Having bought a copy of Inferno a few years ago and played with it, it didn't feel like a mature platform.)
Limbo was
I fixed it for you.