Logic

Question 1

What is the purpose of logic?

Answer 1

To carry out precise and rigorous arguments about assertions and proofs, and to implement these assertions and proofs. We need a language whose structure (syntax) can be precisely described and whose meaning (semantics) can be unambiguously defined.

Question 2

What are the three components of a system of logic?

Answer 2

Syntax: The definition of the formulae of the logic

Semantics: The association of meaning and truth to the formulae of the logic

Proof system: The manipulation of formulae according to a system of rules

All true should be provable (completeness), and all formulae that are provable should be true

Question 3

What are formal methods?

Answer 3

The use of mathematically-based techniques to prove that programs have certain properties

Question 4

What is model checking?

Answer 4

A branch of formal methods where a computer system is first modelled on some mathematical structure, and then a specific property that this system might have is expressed by a formula of some logic. Then we computationally verify whether the particular formula is satisfied by the mathematical model

Question 5

Where is model checking used?

Answer 5

In microprocessor design, design of data communications protocol software, critical software, operating system device drivers

Question 6

What is propositional logic?

Answer 6

A logic which consists of propositions: declarative sentences which are either true or false, and are represented with propositional variables (usually letters) which can take the value T or F

Question 7

Propositional logic symbols

Answer 7

^ = and
v = or
¬ = not
=> = implies
<=> = if and only if

(p => q) is the same as (¬p v q)

Question 8

P => Q truth table

Answer 8

T => T is true
T => F is false
F => T is true
F => F is true

Question 9

P <=> Q truth table

Answer 9

T <=> T is true
T <=> F is false
F <=> T is false
F <=> F is true

Question 10

What is a literal?

Answer 10

Either a propositional variable or its negation

Question 11

What does it mean when a propositional formula φ(x1, x2, …, xn) evaluates to T under f (an assignment of true or false to x1, x2, …, xn)

Answer 11

The row of the truth table for φ corresponding to f evaluates to T. If φ evaluates to T for all f, it’s a tautology, if it evaluates to F for all f it’s a contradiction

Question 12

Distributive Law of Disjunction over Conjunction

Answer 12

a v (b ^ c) = (a v b) ^ (a v c)
(and the same with opposite signs)

Question 13

Generalised distributive law

Answer 13

X ^ (Y1 v Y2 v Y3 v … v Yn)
= (X ^ Y1) v (X ^ Y2) v (X ^ Y3) v … v (X ^ Yn)

Question 14

What does it mean if a set C of logical connectives is functionally complete?

Answer 14

If any propositional formula is equivalent to one constructed using only the connectives from C

Question 15

What does it mean if a propositional formula is in disjunctive normal form?

Answer 15

It consists of an OR of ANDs (e.g. (A ^ ¬B) v (C ^ ¬D) )
Every formula of propositional logic is equivalent to a formula in disjunctive normal form (a disjunction of conjunctions of literals)
You form this DNF formula by looking at which rows of the truth table evaluate to true, joining the literals with ^ and the rows with ^.

Question 16

What is the SAT problem?

Answer 16

Deciding if a propositional formula has a truth assignment that causes it to be true (NP-complete)

Question 17

What is the aim of SAT-solving?

Answer 17

To encode a problem X as a propositional formula φ, so that a solution to X corresponds to φ having a satisfying truth assignment

To employ algorithms to solve the SAT problem

Question 18

What is the k-SAT problem?

Answer 18

The SAT problem but all the clauses contain k literals. k-SAT is polynomial time if k=2, but NP-complete for k >= 3

Question 19

What is the (k,s)-SAT problem?

Answer 19

The SAT problem but every variable appears in at most s clauses

Question 20

What is an argument form?

Answer 20

A sequence of formulae φ1, φ2, …, φn, ψ
It is valid if: whenever a truth assignment f makes φ1, φ2, … φn all evaluate to true, it also makes ψ evaluate to true

This can also be written as φ1, φ2, …, φn├ ψ (sequent)

The rules of inference corresponding to the argument form is φ1, φ2, …, φn => ψ

Question 21

What is modus ponens?

Answer 21

A rule of inference which states that (p ^ (p=>q) => q
p, p=>q, ψ=q

Question 22

What is modus tollens?

Answer 22

¬q, p=>q, ψ=¬p
If p implies q, and q is false, then p is false

Question 23

What is hypothetical syllogism?

Answer 23

p=>q, q=>r, ψ= p=>r
If p implies q, and q implies r, then p implies r

Question 24

What is resolution?

Answer 24

If p v q is true, and ¬p v r is true, then q v r is true

Question 25

Rules for conjunction

Answer 25

^-i (^-introduction)
φ1 φ2
φ1 ^ φ2

^-e1 and ^-e2 (^-elimination)
φ1 ^ φ2
φ1

φ1 ^ φ2
φ2

Question 26

Rules for double negation

Answer 26

¬¬i (¬¬-introduction)
φ
¬¬φ

¬¬e (¬¬-elimination)
¬¬φ
φ

Question 27

Prove the sequent:
p, ¬¬(q^r) ├ ¬¬p^r

Answer 27

1. p (premise)
2. ¬¬(q^r) (premise)
3. ¬¬p (¬¬i 1)
4. q^r (¬¬e 2)
5. r (^e2 4)
6. ¬¬p ^ r (^i 3 5)

Question 28

Rules for implication

Answer 28

=>e (eliminating implication)
φ1 φ1 => φ2
φ2

=>i (introducing implication)

<open>
φ1
<continue>
φ2
<close>
φ1 => φ2

Once the box has been closed, the formulae inside can no longer be used
</close></continue></open>

Question 29

What is a truth assignment?

Answer 29

An assignment of values (true or false) to variables in a formula
A truth assignment satisfies a formula if it makes it evaluate to true
A formula is satisfying if a truth assignment satisfies it

Question 30

What does it mean if a formula B is a logical consequence of a formula A?

Answer 30

Every truth assignment that satisfies A also satisfies B
We can also say that A entails B, or A |= B

We have A |= B if and only if A and not(B) is unsatisfiable

A1, A2, …, An |= B if and only if A1 and A2 … and An and not(B) is unsatisfiable

Checking for entailment/consequence is the same as checking for (un)satisfiability

Question 31

What are literals and clauses?

Answer 31

Literals are variables (x, y, z) and their negations (!x, !y, !z)
Clauses are formulae of the form L1 or L2 or L3 where each L is a literal. They can be thought of as a set.

Question 32

What does it mean if a propositional formula is in conjunctive normal form?

Answer 32

It consists of an AND of ORs (e.g. (A v ¬B v C) ^ (D ^ ¬E) )
Every formula of propositional logic is equivalent to a formula in conjunctive normal form (a conjunction of clauses)
Each CNF is a clause-set

Question 33

DIMACS format

Answer 33

Text format for representing clause sets
Variables are indicated as positive integers, negated variables are represented by negative integers
Any line starting with a c is a comment
At the top of the file is a line of form “p cnf N M” where N is the number of the largest variable, and M is the total number of clauses in the clause set
Clauses are separated by a zero

Question 34

How would the clause set F = {{u, ¬v, ¬y}, {¬u, z}, {¬v, ¬w}, {w, ¬x}, {x, y, ¬z}} be represented?

Answer 34

c VGE
c BBC
c HRT
c 5 because there are 5 clauses, 6 because there are 6 unique variables u, v, w, x, y, z
p cnf 6 5
1 -2 -5 0
-1 6 0
-2 -3 0
3 -4 0
-4 5 -6 0

Question 35

Procedure for converting a formula to CNF?

Answer 35

Express all connectives using ^, v and ¬
Push ¬ inside
Use De Morgan’s Laws to convert to CNF

Question 36

Tseitin’s algorithm for converting a propositional formula to CNF

Answer 36

Input: a propositional formula A. Let F = ∅

While A has a subformula LM where * is any binary logical connective and L and M are literals:
- Replace this subformula with a new variable x(LM)
- Append “V F(x(L*M))” to the end of F (see the flashcard “defining clause-sets”)

Now A is a single literal B. Add “V B” to F and halt. Output clause set F.

Question 37

Defining clause sets