Symbolic Logic

Symbolic Logics: Symbolic logic is a collection of languages that use symbols to represent facts, events, and actions, and provide rules to symbolize reasoning. Given the specification of a system and a collection of desirable properties, both written in logic formulas, we can attempt to prove that these desirable properties are logical consequences of the specification. In this section, we introduce the propositional logic (also called propositional calculus, zero-order logic, digital logic, or Boolean logic, the most simple symbolic logic), the predicate logic (also called predicate calculus or first-order logic), and several proof techniques.

Propositional Logic
Using propositional logic, we can write declarative sentences called propositions that can be either true (denoted by T) or false (denoted by F) but not both.We use an uppercase letter or a string of uppercase letters to denote a proposition.

Example
P denotes “car brake pedal is pressed”
Q denotes “car stops within five seconds”
R denotes “car avoids a collision”
These symbols P, Q, and R, used to represent propositions, are called atomic formulas, or simply atoms. To express more complex propositions such as the following compound proposition, we use logical connectives such as→(if-then or imply): “if car brake pedal is pressed, then car stops within five seconds.”

This compound proposition is expressed in propositional logic as:
P → Q
Similarly, the following statement
“if car stops within five seconds, then car avoids a collision” is expressed as:
Q → R
Given these two propositions, we can easily show that P → R, that is,
“if car brake pedal is pressed, then car avoids a collision.”
We can combine propositions and logical connectives to form complicated formulas.

A well-formed formula is either a proposition or a compound proposition formed accoding to the following rules.
Well-Formed Formulas: Well-formed formulas in propositional logic are defined recursively as follows:
1. An atom is a formula.
2. If F is a formula, then (¬F) is a formula, where ¬ is the not operator.
3. If F and G are formulas, then (F ∧G), (F ∨G), (F → G), and (F ↔ G) are formulas. (∧ is the and operator, ∨ is the or operator,↔stands for if and only if or iff.)
4. All formulas are generated using the above rules.

Some parentheses in a formula can be omitted for conciseness if there is no ambiguity.

 

 

 

 

 

 

 

Interpretation: An interpretation of a propositional formula G is an assignment of truth values to the atoms A1, . . . , An in G in which every Ai is assigned either T or F, but not both.

Then a formula G is said to be true in an interpretation iff G is evaluated to be true in the interpretation; otherwise, G is said to be false in the interpretation. A truth table displays the the truth values of a formula G for all possible interpretations of G. For a formula G with n distinct atoms, there will be 2n distinct interpretations for G. Figure 2.1 shows the truth table for P → R. Figure 2.2 shows the truth table for several simple formulas.

A formula is valid iff it is true under all its interpretations. A formula is invalid iff it is not valid. A formula is unsatisfiable (inconsistent) iff it is false under all its interpretations. A formula is satisfiable (consistent) iff it is not unsatisfiable.

A literal is an atomic formula or the negation of an atomic formula. A formula is in conjunctive normal form (CNF) if it is a conjunction of disjunction of literals and can be written as

where n ≥ 1; m1, . . . ,mn ≥ 1; and each Li, j is a literal.
A formula is in disjunctive normal form (DNF) if it is a disjunction of conjunction of literals and can be written as

where n ≥ 1; m1, . . . ,mn ≥ 1; and each Li, j is a literal. These two normal forms make it easier for proof procedures to manipulate and analyze logic formulas. Fig