Skip to main content

Propositional Logic

Syntax

The syntax of propositional logic defines the allowable sentences. The atomic sentences consist of a single proposition symbol. Each such symbol stands for a proposition that can be true or false. We use symbols that start with an uppercase letter and may contain other letters or subscripts.

There are two proposition symbols with fixed meanings: True is the always-true proposition and False is the always-false proposition.

Complex sentences are constructed from simpler sentences, using parentheses and operators called logical connectives:

  • negation: If $\alpha$ is a sentence, $\neg\alpha$ is a sentence
  • conjunction: If $\alpha$ and $\beta$ are sentences, $\alpha \land \beta$ is a sentence
  • disjunction: If $\alpha$ and $\beta$ are sentences, $\alpha \lor \beta$ is a sentence
  • implication: If $\alpha$ and $\beta$ are sentences, $\alpha \implies \beta$ is a sentence
  • biconditional: If $\alpha$ and $\beta$ are sentences, $\alpha \iff \beta$ is a sentence

Validity and satisfiability

A sentence is valid if it is true in all models. Validity is connected to entailment via the deduction theorem: $KB \models \alpha$ if and only if $KB \implies \alpha$ is valid.

  • A sentence is satisfiable if it is true in some model
  • A sentence is unsatisfiable if it is true in no models
  • Satisfiability is connected to entailment via the following (refutation or contradiction): $KB \models \alpha$ if and only if $KB \land \lnot\alpha$ is unsatisfiable

Inference procedures for propositional logic

Our goal now is to decide whether $KB \models \alpha$ for some sentence $\alpha$.

Model checking

Reasoning with truth tables

Reasoning with truth tables is a form of semantic reasoning, in the sense that it directly exploits the definition of entailment: 𝛼 ⊨ 𝛽 holds when 𝛽 in every model that makes 𝛼 true.

In PL, a model is an assignment of truth values (1 or 0, true or false, 𝑇 or ⊥) to every propositional symbol that appears in 𝛼 or 𝛽 (or both)

Therefore, with 𝑛 symbols we have 2𝑛 different models, which correspond to the rows of the truth table

For every model (row), we compute the truth vales of 𝛼 and 𝛽 (by recursively computing the truth values of all the subsentences of 𝛼 and 𝛽) Then we have that 𝛼 ⊨ 𝛽 if, and only if, every model (row) that assigns 1 to 𝛼 also assigns 1 to 𝛽

Properties

This reasoning procedure is sound and complete. It always terminates, making reasoning in PL decidable.

However, it is inefficient when many propositional symbols are involved, because it has to compute a table of size 2𝑛×𝑀, where 𝑛 is the number of propositional symbols and 𝑀 is the number of subsentences the appear in the premises and the conclusion

Propositional satisfiability

Certain applications of PL require an agent to establish whether a set of sentences 𝛼 is or is not satisfiable

The problem of establishing the satisfiability of a set of propositional sentences is known as SAT Many interesting problems, including establishing propositional entailment, can be reduced to SAT

A (rather inefficient) solution of SAT is given by truth tables: 𝛼 is satisfiable if, and only if, it has truth value 1 in at least one row of its truth table

DPLL

Establish whether a set of sentences 𝛼 is or is not satisfiable

Preprocessing: convert every sentence in CNF (Conjunctive Normal Form)

Body of the procedure: from an empty assignment, incrementally try to build a model of 𝛼

  • if a model is built, 𝛼 is satisfiable
  • if the algorithm terminates without being able to build a model, 𝛼 is unsatisfiable
Back to top