First order logic in practice, how to deal with undecidablity?

Question

I am very new to these things. Hope this is not a very naive question.

I tried the following formula in Prolog: A ⇒ B

and given that B is true, I evaluate A and it says FALSE.

My question is why FALSE? (why not TRUE?) Given the current information we don't know anything about B. Does Prolog work based on the assumption that for anything unknown, it outputs FALSE?

If this is an assumption, how common is this?

Another thing that comes into mind is that, it is finding the assignment to the conjunction of input query and axioms (basically SAT solving). Since the resulting output is TRUE, regardless of whatever value A has, it just chooses one randomly (or zero by default?).

Based the properties of the 1st order logic, it is semidecidable. if a sentence A logically implies a sentence B then this can be discovered, but not the other way around. So, how the latter case is handled in practice, when there is no proof of TRUTH?

PS1. A little explanation about how Prolog works, might also be useful. Does it use SAT solvers as black box? Or greedy search algorithms?

Answer 1

Does Prolog work based on the assumption that for anything unknown, it outputs FALSE?

Yes, it certainly does. This behavior reflects the Closed-World Assumption (CWA) in that if a fact isn't explicitly stated, it is considered false.

If this is an assumption, how common is this?

Very common -- most databases use this assumption.

It may help you to learn about Prolog's method of inference: SLD Resolution.