How can a knowledge base support a proof?

"Knowledge bases in artificial intelligence systems are designed to support these chains of reasoning. They contain statements expressed in formal logic that can be examined to deduce only the new facts that logically follow from the old. Suppose, for instance, that we had a knowledge base that currently contained the following facts: 1. A ⇒ C 2. ¬ (C ∧ D) 3. (F ∨¬ E) ⇒ D 4. A ∨ B. These facts are stated in propositional logic, and we have no idea what any of the propositions really mean, but then neither does the computer, so hey. Fact #1 tells us that if proposition A is true, then we know C is true as well. Fact #2 tells us that we know C ∧ D is false, which means at least one of the two must be false. And so on. Large knowledge bases can contain thousands or even millions of such expressions. It’s a complete record of everything the system “knows.” Now suppose we learn an additional fact: ¬ B. In other words, the system interacts with its environment and comes to the conclusion that proposition B must be false. What else, if anything, can now be safely concluded from this? It turns out that we can now conclude that F is also false. How do we know this? Here’s how: 1. Fact #4 says that either A or B (or both) is true. But we just discovered that B was false. So if it isn’t B, it must be A, and therefore we conclude that A must be true. For the curious, this rule of common sense is called a “disjunctive syllogism.” 2. Now if A is true, we know that C must also be true, because fact #1 says that A implies C. So we conclude that C is true. This one goes by the Latin phrase “modus ponens.” 3. Fact #2 says that C ∧ D must be false. But we just found out that C was true, so it must be D that’s false in order to make the conjunction false. So we conclude that D is false. This is a disjunctive syllogism in disguise, combined with De Morgan’s law. 4. Finally, fact #3 tells us that if either F were true or E were false, then that would imply that D would be true. But we just found out that D is false. Therefore, neither F nor ¬ E can be true. This step combines “modus tollens” with “disjunction elimination.” So we conclude that F must be false. Q.E.D. The letters “Q.E.D.” at the end of a proof stand for a Latin phrase meaning, “we just proved what we set out to prove.” It’s kind of a way to flex your muscles as you announce that you’re done."