In a LogicProgramming system (or a RelationalDatabase, or a ConstraintProgramming system, etc); one builds a collection of facts (things held to be true) and axioms (rules for deriving additional facts from the set of base facts).
If a theorem can be shown to be true based on the facts and axioms; then it is true.
How do you handle a query that cannot be shown from the above (in other words, isn't derivable?)
Two possibilities, the ClosedWorldAssumption and the OpenWorldAssumption.
The ClosedWorldAssumption holds that anything that cannot be shown to be true is false; no explicit declaration of falsehood is needed. Consequently, any query (which terminates) will either return true or false; there is no possibility of "unknown".
- Technically, one can ask the system to prove that something is Unknown, or to prove that something is Known, so long as there is a means to represent such a query. It is not a violation of the ClosedWorldAssumption to have facts of the sort Known(X) and Unknown(Y), or even axioms like Forall X: (SomePredicate(X)-> Unknown(OtherPredicate(X))), Forall X: X<->Known(X), etc. The ClosedWorldAssumption does not enforce restrictions on the sort of logic used. However, it cannot answer 'unknown' directly; to make use of such, you'd need to craft your queries correctly -- ask Known(P), or Known(Unknown(P)).
- The real difficulty with the ClosedWorldAssumption is that you cannot add information. Everything is known a priori. One cannot assert "oh, yeah! X is known!" without creating a new world and adding this fact to that world, along with all the other facts except the one that said: Unknown(X), which would need to be removed. (If this is done regularly, one would be wise to utilize ModalLogic?, where reasoning over worlds can happen). This is less a problem with the OpenWorldAssumption, where 'unknown' isn't expressed as a fact in the database, but rather as the absence of a fact. --db
Most programming systems which use logic or predicate calculus use the
ClosedWorldAssumption, including:
CategoryLogic
Closed World Assumption