and related results that show there is not a procedure which can prove all true statements in logic + arithmetic, arithmetic matters of course because we need to handle dimensions, money, etc. This doesn't mean you can't solve the problem in front of you much of the time but it's not like a SQL server which has a definite algorithm to return all the answers all the time in a finite time.
covers a wide range of practical problems that turn up such as reasoning about other people's beliefs, about things that were true in the past or will be true in the future, things that are possible, things that are necessary, etc. People build modal logics that can handle one of these things but there is no "standard" that handles all of them.
Logical negation is tricky. You might know P or you might know ¬P but maybe you don't know anything about P. For some cases you want to query for "There is no evidence for P", other times you want to query for a solid "P". You definitely don't want a system that spends a lot of time enumerating all the things it can't prove though because that's endless
Reasoning over probability is essential in our imperfect world. You might think the system could store
P 80% probability
¬P 20% probability
but probabilities in the real world are conditional so it is maybe
P Q 10%
¬P Q 35%
P ¬Q 25%
¬P ¬Q 30%
which is not so bad but if you have hundreds of predicates the problem gets intractable but it's essential if you want to make a medical diagnosis, disambiguate the sense of a word, etc. (Note this problem relates to machine learning where it is all about learning a probability distribution, you can't get enough samples to measure every "cell" of the joint probability distribution, practical machine learning algorithms make good guesses)
There also is the problem of keeping the database consistent over time as it changes, see
There are a lot of answers to these problems that will please some people some of the time but there's nothing like the C programming language or Linux that anybody can pick up and start working with.
https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
and related results that show there is not a procedure which can prove all true statements in logic + arithmetic, arithmetic matters of course because we need to handle dimensions, money, etc. This doesn't mean you can't solve the problem in front of you much of the time but it's not like a SQL server which has a definite algorithm to return all the answers all the time in a finite time.
Different variations of
https://en.wikipedia.org/wiki/Modal_logic
covers a wide range of practical problems that turn up such as reasoning about other people's beliefs, about things that were true in the past or will be true in the future, things that are possible, things that are necessary, etc. People build modal logics that can handle one of these things but there is no "standard" that handles all of them.
Logical negation is tricky. You might know P or you might know ¬P but maybe you don't know anything about P. For some cases you want to query for "There is no evidence for P", other times you want to query for a solid "P". You definitely don't want a system that spends a lot of time enumerating all the things it can't prove though because that's endless
Reasoning over probability is essential in our imperfect world. You might think the system could store
but probabilities in the real world are conditional so it is maybe which is not so bad but if you have hundreds of predicates the problem gets intractable but it's essential if you want to make a medical diagnosis, disambiguate the sense of a word, etc. (Note this problem relates to machine learning where it is all about learning a probability distribution, you can't get enough samples to measure every "cell" of the joint probability distribution, practical machine learning algorithms make good guesses)There also is the problem of keeping the database consistent over time as it changes, see
https://en.wikipedia.org/wiki/Reason_maintenance
There are a lot of answers to these problems that will please some people some of the time but there's nothing like the C programming language or Linux that anybody can pick up and start working with.