Representation - propositional logic
We begin our course by studying propositional logic. After we introduce the definitions, we will discuss satisfiability in propositional logic and then move on to state of the art techniques to solve systems specified with propositional logic.
Propositional logic is a formal language used to specify knowledge in a mathematically rigorous way. We first define the syntax (grammar) and then the semantics (meaning) of sentences in propositional logic.
We denote our propositional variables by where each is a binary variable that can be true or false.
Sentences are defined recursively as follows:
- A propositional variable is a sentence (this is known as an atomic sentence)
- If and are sentences, then , , and are valid sentences
For example, is a valid sentence while isn’t a valid sentence.
We have to define the notion of a world. A world is an assignment of a truth value to each propositional variable. Note that there are possible worlds if we have propositional variables.
We determine if a sentence is true in a world using the following recursive rules:
- if and only if is true
- if and only if
- if and only if () OR ()
- if and only if () AND ()
- (Note that is syntactic sugar for , and we can use the rules above)
For example, is true in any world while is never true in any world.
A knowledge base is a collection of sentences that we know are true, i.e. . The sentences in the knowledge base allows us to compactly specify the allowable states of the world. By adding new sentences, the number of possible worlds consistent with our knowledge base could decrease (if we gain new information), go to zero (if the new sentence is inconsistent with the existing knowledge base), or remain the same (if the new sentence is entailed by existing sentences).
Figure: By adding to our KB , the number of possible worlds can (i) decrease, (ii) go to zero, or (iii) remain the same.
We will make use of the following definitions:
- A sentence is satisfiable (consistent) if there exists at least one world that makes the sentence true, i.e. .
- A sentence is valid if the sentence is true in every possible world, i.e. .
- Two sentences are equivalent if they are true in the same models, e.g. and .
Inference reduces to satisfiability
The basic inference problem in the propositional logic system is the following: given the knowledge that we have about the world, is it the case that some property must always hold? In other words, what conclusion can we reach about some other sentence? The three possible cases that could result are always true, depends, and always false.
Inference problem: Does ? We can solve this by checking if is satisfiable.
- If not satisfiable, then we know that . This is similar to the idea behind proof by contradiction.
- If satisfiable, then there are two possible cases. Check if is satisfiable. If is satisfiable, then there is no definitive answer. If is not satisfiable, then we know that .
Many problems across different domains can be encoded using propositional logic. Inference in this space basically boils down to checking satisfiability. For examples, problems such as solving Sudoku puzzles, hardware verification, and planning can be encoded as satisfiability problems and then solved efficiently using state of the art satisfiability solvers. Since a lot of research has gone into improving general SAT solvers, if some domain-specific problem has an efficient transformation into an instance of satisfiability checking, then SAT solvers can often solve these domain-specific problems efficiently.
Conjunctive normal form
To check the satisfiability of a sentence, the first step is to convert sentences into normal form which is easier for satisfiability solvers to handle. A sentence is in conjunctive normal form (also known as clausal norm form or CNF) if a sentence is a conjunction of disjunctions.
Given any formula, we can always convert it into CNF using the following procedure:
- The first step is to remove syntactic sugar, e.g. change into . After this step, we should only have negations, conjunctions, and disjunctions.
- Push negations in. Negations should only appear in front of propositional variables. For example, change into and into .
- Distribute disjunctions over conjunctions, e.g. change into . (Note that converting a sentence which is composed of many disjunctions of conjunctions into CNF using this procedure can create an exponential number of clauses.)
Checking if an assignment satisfies a CNF formula is easy. A clause is satisfiable if and only if at least one of the literals (a variable or the negation of a variable) is set to true. A sentence is satisfiable if and only if each clause is satisfiable.
Suppose we want to test the satisfiability of a formula in CNF. Consider what happens when we set a propositional variable to true. If P does not belong to a given clause, then that clause is unaffected. If P belongs to a given clause, then that clause becomes satisfied and we can remove that clause from the formula. The resulting formula can be expressed as .