Limbo – A Reasoning System for First-Order Limited Belief(github.com)
github.com
Limbo – A Reasoning System for First-Order Limited Belief
https://github.com/schwering/limbo
26 comments
Has anyone seen logic systems that are able to reason about probabilities? As far as I understand Limbo (and other logic systems) are limited to saying something is true or false, but unable to say that something has X% chance of being true.
Take a look at Distributed Situation-state Spaces [1].
[1] http://www.let.rug.nl/festschriftnerbonne/08.%20Brouwer%20et...
[1] http://www.let.rug.nl/festschriftnerbonne/08.%20Brouwer%20et...
What about fuzzy logic? It's not giving you probabilities of something being true; rather, it gives you a measure "how true" something is (rather than being 100% true or 100% false).
Something like ProbLog https://dtai.cs.kuleuven.be/problog/ ?
On the bottom links under 'Tools' there are some related systems as well.
On the bottom links under 'Tools' there are some related systems as well.
That seems neat. I'll have to try and see if I can model my problem with that.
See also cplint and the included example programs, using both regular Prolog and probabilistic extensions:
http://cplint.lamping.unife.it/example/examples.swinb http://cplint.lamping.unife.it/example/inference/inference_e...
The github repository of cplint is:
https://github.com/friguzzi/cplint
http://cplint.lamping.unife.it/example/examples.swinb http://cplint.lamping.unife.it/example/inference/inference_e...
The github repository of cplint is:
https://github.com/friguzzi/cplint
This is pretty interesting. How would this be different from traditional knowledge base programs? Is it that you are explicitly modelling beliefs and actions and things like that?
Would anyone be willing to explain what's different between this & how humans make decisions?
First, we'd have to have a good model for human decision making.
If we were to start with this as the foundation for modeling human decisions, where does this fail as a model?
Its kind of hard to do the measurements necessary to answer that question without being able to accurately and objectively measure actual human beliefs (which may not be the same as self-reported beliefs.)
Ok. What about using inaccurate, subjective measures? How well does it model self-reported beliefs?
What resolution are you looking for? All models fail to be the thing they're modelling.
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.
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.
"What sort of predictions that this makes are contradicted by observation"?
This is what I meant. Thanks for providing the clarification I didn't think to include.
I thought the clarification to be self-evident, for what it's worth.
Hah! Good one!
Nice try, Bezos!
Nice try, Bezos!
Thanks for this comment. I can't wait to see what the system says about how to market to those who'll create a new HN name for the sake of doxxing someone!
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.
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.
This is probably a really dumb question, but... ELI5? I understood effectively none of that readme, and the web demos didn't really help, either.
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 "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."
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."
Limbo is a programming language for writing distributed systems and is the language used to write applications for the Inferno operating system. It was designed at Bell Labs by Sean Dorward, Phil Winterbottom, and Rob Pike. Google the name of your project before naming it .
I'm going to be slightly unorthodox and say that as long as they're no embarking on the same type of venture, having the same name is more-or-less okay. Nobody with domain-specific knowledge is going to be confused by this, and it's barely even worth picking a fight over. If he wants to call it Limbo, I say let him.
See also Newsqueak (also Rob Pike) and the Squeak implementation of smalltalk.
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.)
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.)
Apparently there are more projects than proper nouns. This just makes life more interesting.
>Limbo is a programming language for writing distributed systems
Limbo was
I fixed it for you.
Limbo was
I fixed it for you.