Logic Flashcards
What is the purpose of logic?
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.
What are the three components of a system of logic?
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
What are formal methods?
The use of mathematically-based techniques to prove that programs have certain properties
What is model checking?
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
Where is model checking used?
In microprocessor design, design of data communications protocol software, critical software, operating system device drivers
What is propositional logic?
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
Propositional logic symbols
^ = and
v = or
¬ = not
=> = implies
<=> = if and only if
(p => q) is the same as (¬p v q)
P => Q truth table
T => T is true
T => F is false
F => T is true
F => F is true
P <=> Q truth table
T <=> T is true
T <=> F is false
F <=> T is false
F <=> F is true
What is a literal?
Either a propositional variable or its negation
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)
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
Distributive Law of Disjunction over Conjunction
a v (b ^ c) = (a v b) ^ (a v c)
(and the same with opposite signs)
Generalised distributive law
X ^ (Y1 v Y2 v Y3 v … v Yn)
= (X ^ Y1) v (X ^ Y2) v (X ^ Y3) v … v (X ^ Yn)
What does it mean if a set C of logical connectives is functionally complete?
If any propositional formula is equivalent to one constructed using only the connectives from C
What does it mean if a propositional formula is in disjunctive normal form?
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 ^.
What is the SAT problem?
Deciding if a propositional formula has a truth assignment that causes it to be true (NP-complete)
What is the aim of SAT-solving?
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
What is the k-SAT problem?
The SAT problem but all the clauses contain k literals. k-SAT is polynomial time if k=2, but NP-complete for k >= 3
What is the (k,s)-SAT problem?
The SAT problem but every variable appears in at most s clauses
What is an argument form?
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 => ψ
What is modus ponens?
A rule of inference which states that (p ^ (p=>q) => q
p, p=>q, ψ=q
What is modus tollens?
¬q, p=>q, ψ=¬p
If p implies q, and q is false, then p is false
What is hypothetical syllogism?
p=>q, q=>r, ψ= p=>r
If p implies q, and q implies r, then p implies r
What is resolution?
If p v q is true, and ¬p v r is true, then q v r is true
Rules for conjunction
^-i (^-introduction)
φ1 φ2
φ1 ^ φ2
^-e1 and ^-e2 (^-elimination)
φ1 ^ φ2
φ1
φ1 ^ φ2
φ2
Rules for double negation
¬¬i (¬¬-introduction)
φ
¬¬φ
¬¬e (¬¬-elimination)
¬¬φ
φ
Prove the sequent:
p, ¬¬(q^r) ├ ¬¬p^r
- p (premise)
- ¬¬(q^r) (premise)
- ¬¬p (¬¬i 1)
- q^r (¬¬e 2)
- r (^e2 4)
- ¬¬p ^ r (^i 3 5)
Rules for implication
=>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>
What is a truth assignment?
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
What does it mean if a formula B is a logical consequence of a formula A?
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
What are literals and clauses?
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.
What does it mean if a propositional formula is in conjunctive normal form?
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
DIMACS format
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
How would the clause set F = {{u, ¬v, ¬y}, {¬u, z}, {¬v, ¬w}, {w, ¬x}, {x, y, ¬z}} be represented?
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
Procedure for converting a formula to CNF?
Express all connectives using ^, v and ¬
Push ¬ inside
Use De Morgan’s Laws to convert to CNF
Tseitin’s algorithm for converting a propositional formula to CNF
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.
Defining clause sets
