SC Chapter 2 Propositional Logic
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 2 Propositional Logic
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 2 Propositional Logic
-
- 1 / 43
-
Cartes-fiches
What is the abstract syntax of propositional logic?
phi := a | \neg phi | (phi \and phi) with a \in AP and phi \in APForm
What is the set AP?
Atomic propositions
What is syntactic sugar? [1+4]
Operators which can be defined with the abstract syntax
1. false // a \land \neg a AND true // a \lor \neg a
2. \or AND \xor
3. →
4. ↔
What is the order of operators for omitting parentheses?
-- || ↔ → \or \and \neg || ++
What is the domain of propositional logic?
B={0,1}
What are the interpretations of propositional logic? [4]
1. \alpha \in Assign : AP → B
2. \alpha \in 2^AP // the named are true the others false
3. \alpha \in {0,1}^AP // if order on the propositions available
4. \alpha \in Truth-Table
What is the lemma in semantic?
If \alpha_1|AP(phi) = \alpha_2|AP(phi)
Then (\alpha_1 satisfies phi) iff (\alpha_2 satisfies phi)
How many binary operators can we define that have different semantics if AP={a,b}?
2^4 = 16 // Because we have 4 different settings for a and b (00, 01, 10, 11) and every setting can be 0 or 1
What is the notation of the satisfaction relation? [3]
1. \alpha |= phi // Called \alpha satisfies or is model for phi OR phi holds for \alpha
2. T |= phi iff T \subseteq sat(phi) // For Interpretations
3. phi_1 |= phi_2 iff sat(phi_1) \subseteq sat(phi_2) // For formulas
What is the recursive definition of the satisfaction relation? [6]
1. \alpha |= a iff \alpha(a) = true
2. \alpha |= \neg phi iff \alpha !|= phi
3. \alpha |= phi1 \and phi2 iff \alpha |= phi1 and \alpha |= phi2
4. \alpha |= phi1 \or phi2 iff \alpha |= phi1 or \alpha |= phi2
5. \alpha |= phi1 → phi2 iff \alpha |= phi1 implies \alpha |= phi2
6. \alpha |= phi1 ↔ phi2 iff \alpha |= phi1 iff \alpha |= phi2
What is the definition of the polynomial algorithm eval(\alpha, phi)? [1+3]
Signiture eval(\alpha, phi) → B
1. If phi = a return \alpha(a)
2. If phi = \neg phi_1 return not eval(\alpha, phi_1)
3. If phi = phi_1 op phi_2 return eval(\alpha, phi_1) op eval(\alpha, phi_2)
What is the notation of the satisfying assignments?
sat : APForm → 2^Assign // every assignment satisfies or not
What is the recursive definition of the satisfying assignments? [4]
1. sat(a) = {\alpha | \alpha(a)=1} with a \in AP
2. sat(\neg phi) = Assign \ sat(phi)
3. sat(phi_1 \land phi_2) = sat(phi_1) \cut sat(phi_2)
4. sat(phi_1 \lor phi_2) = sat(phi_1) \cup sat(phi_2)
What is the equivalence of satisfying assignments?
\alpha |= phi iff \alpha \in sat(phi)
What is the definition of validity and tautology?
If sat(phi) = Assign then we write |= phi
What are examples of validity and tautology? [6]
1. a \land 1 ↔ a
2. a \land 0 ↔ 0
3. \neg \neg a ↔ a // double negation
4. a \land (b \lor c) ↔ (a \land b) \lor (a \land c)
5. \neg (a \land\lor b) ↔ (\neg a \lor\land \neg b) // De Morgan
6. (a → b) ↔ \neg a \lor b
What is the definition of not valid?
If sat(phi) != Assign then we write !|= phi
What is the definition of satisfiable?
If sat(phi) != {} AND !|= \neg phi
What is the definition of unsatisfiable and contradiction?
If sat(phi) = {} AND |= \neg phi
What is the definition of decision procedure?
Terminates for each formulae phi with the correct answer
What is the Cook’s theorem?
Decision procedure is decidable but NP-complete
What is modeling of propositional logic used for? [5]
1. Logistics
2. Planning
3. Electronic design
4. Automotive industry
5. Cryptography
What is the definition of literal?
Variable or negated variable
What is the definition of term?
Conjunction of literals
What is the definition of clause?
Disjunction of literals
What is the definition of the negation normal form (NNF)?
Only \neg before literals, \land and \lor
What is the definition of the conversion into NNF? [3]
1. linear time
2. eliminate all other connectives
3. push negations to literals with double negation and de morgan
What is the definition of the disjunctive normal form (DNF, special case of NNF)?
Disjunction of terms (OU)
What is the definition of the conversion into DNF? [4]
1. exponential time but satisfiability check in linear time and space
2. convert to NNF
3. eliminate \lor
4. 2^n clauses
What is the definition of the conjunctive normal form (CNF, special case of NNF)?
Conjunction of clauses (UO)
What is the definition of the conversion into CNF? [4]
1. exponential time
2. convert to NNF
3. eliminate \land
4. 2^n clauses and 2n variables
What is the definition of the conversion into CNF using Tseitin’s encoding? [4]
1. linear time
2. formulae are not equivalent but equi-satisfiable
3. add auxiliary variables for gates with up to 4 constraints
4. 3n+1 clauses and 3n variables
What is the definition of enumeration? [2]
1. Enumerate possible solutions with truth tables
2. Not possible with every logic
What is the definition of the first algorithm of enumeration? [1+2]
Signiture sat(phi) → boolean // complete assignment
1. For all \alpha \in Assign
2. If eval(\alpha, phi) return true
3. Return false
What is the definition of the second algorithm of enumeration?
phi iff phi_[0/a] \lor phi_[1/a] // Partial assignment
What is the definition of deduction?
Use a proof system to derive the satisfiability of a formula with a set of premises
What is the definition of an inference rule?
[Antecedents] / [Consequents] (rule)
What is the definition of an axiom?
[No Antecedents] / [Consequents] (H_i)
What is the definition of a proof system?
A set of axioms and inference rules
What is the definition of soundness? [3]
1. Are all derived conclusions “correct” from premises
2. If |-_H phi then |= phi
3. Is soundness of of axioms // easy with truth tables
