Model Checking Algorithm

• To determine if KB ⊨ α (in other words, answering the question: “can we conclude that α is true based on our knowledge base”)
  • Enumerate all possible models.
  • If in every model where KB is true, α is true as well, then KB entails α (KB ⊨ α).

However, model Checking is not good, since it is slow → $2^n$

Sample Code

def check_all(knowledge, query, symbols, model):
 
    # If model has an assignment for each symbol
    # (The logic below might be a little confusing: we start with a list of symbols. The function is recursive, and every time it calls itself it pops one symbol from the symbols list and generates models from it. Thus, when the symbols list is empty, we know that we finished generating models with every possible truth assignment of symbols.)
    if not symbols:
 
        # If knowledge base is true in model, then query must also be true
        if knowledge.evaluate(model):
            return query.evaluate(model)
        return True
    else:
 
        # Choose one of the remaining unused symbols
        remaining = symbols.copy()
        p = remaining.pop()
 
        # Create a model where the symbol is true
        model_true = model.copy()
        model_true[p] = True
 
        # Create a model where the symbol is false
        model_false = model.copy()
        model_false[p] = False
 
        # Ensure entailment holds in both models
        return(check_all(knowledge, query, remaining, model_true) and check_all(knowledge, query, remaining, model_false))

Related

• Knowledge Engineering