Java · Course navigation

Java: propositional entailment by model checking

Enumerate every truth assignment to decide whether a knowledge base entails a query.

On this page

Before you start

Java loops and boolean operators.

Enumerate every truth assignment to decide whether a knowledge base entails a query.
Predict the sample output and explain the state changes.
Complete the practice task and check the boundary cases.

The concept

A knowledge base is a set of sentences. In propositional logic, a model assigns true or false to every symbol. A sentence is entailed by the knowledge base if it is true in every model where the whole knowledge base is true.

The program checks the rules P implies Q, Q implies R, and the fact P. It enumerates all 8 models using the bits of a counter, keeps those that satisfy the knowledge base, and tests two queries. R is true in every such model, so it is entailed, and not-R is false in all of them, so it is not.

Code example

Java

class Main {
  public static void main(String[] args) {
    boolean entailsR = true;
    boolean entailsNotR = true;
    int models = 0;
    for (int bits = 0; bits < 8; bits++) {
      boolean p = (bits & 1) != 0;
      boolean q = (bits & 2) != 0;
      boolean r = (bits & 4) != 0;
      boolean kb = (!p || q) && (!q || r) && p;
      if (kb) {
        models++;
        if (!r) {
          entailsR = false;
        }
        if (r) {
          entailsNotR = false;
        }
      }
    }
    System.out.println("models of KB: " + models);
    System.out.println("KB entails R: " + entailsR);
    System.out.println("KB entails not R: " + entailsNotR);
  }
}

Output

models of KB: 1
KB entails R: true
KB entails not R: false

Example details

Follow the code

Open the walkthrough to inspect the example one step at a time.

Show guided walkthrough

Guided walkthroughReady

1class Main {

2 public static void main(String[] args) {

3 boolean entailsR = true;

4 boolean entailsNotR = true;

5 int models = 0;

6 for (int bits = 0; bits < 8; bits++) {

7 boolean p = (bits & 1) != 0;

8 boolean q = (bits & 2) != 0;

9 boolean r = (bits & 4) != 0;

10 boolean kb = (!p || q) && (!q || r) && p;

11 if (kb) {

12 models++;

13 if (!r) {

14 entailsR = false;

15 }

16 if (r) {

17 entailsNotR = false;

18 }

19 }

20 }

21 System.out.println("models of KB: " + models);

22 System.out.println("KB entails R: " + entailsR);

23 System.out.println("KB entails not R: " + entailsNotR);

24 }

25}

Follow the example

Start to inspect the source, values, and output. These prepared steps explain the published sample; grouped loop steps describe multiple iterations.

View the complete dry-run table

Prepared trace of the published program. Some rows group repeated iterations.
What happens	State after step	Output so far
Three symbols give 2³ = 8 possible models.	`—`	—
P implies Q is the same as not-P or Q. The fact P must also hold.	`only P=Q=R=true satisfies all three`	—
A model of the KB where R is false would disprove entailment. None exists, so this never runs.	`only P=Q=R=true satisfies all three`	—
Exactly one model satisfies the knowledge base.	`models = 1`	models of KB: 1
R holds in the only model, so not-R is not entailed.	`models = 1`	models of KB: 1 KB entails R: true KB entails not R: false

Behind the scenes

How Java processes this code

The Java compiler produces bytecode. The JVM loads the class and invokes its main method.

Cost and common mistakes

O(2ⁿ · k) time for n symbols and a knowledge base of size k.

Model checking takes 2^n steps for n symbols, so it is only practical for small problems. SAT solvers and resolution scale better.
Entailment is not the same as truth in one model: the query must be true in all models of the KB.

Try it yourself

What happens if you remove the fact p from the knowledge base?

Reveal answer and reasoning

More models satisfy the KB, including ones where R is false, so R is no longer entailed.