SC Chapter 2 Propositional Logic

Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 2 Propositional Logic

0.0 (0)

R. B.

Étudier

R. B.

À propos de ce fichier

This flashcard set delves into the fundamentals of propositional logic at a university level, focusing on definitions, algorithms, and applications. It covers key concepts like resolution inference rules, proof systems, satisfiability, and normal forms, including CNF and DNF. The flashcards also explore the conversion processes, such as Tseitin’s encoding, and discuss the practical uses of propositional logic in various fields like logistics, planning, and cryptography. Ideal for computer science students, this collection provides a comprehensive overview of the theoretical and practical aspects of propositional logic, making it invaluable for those looking to deepen their understanding of this critical area.

Cartes-fiches

Utilisateurs

Langue

Anglais

Catégorie

Informatique

Niveau

Université

Créé / Mis à jour

18.02.2017 / 25.02.2017

Fichiers de cartes similaires

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

What is the definition of completeness? [2]

1. Are all “correct” conclusions from premises derived

2. If |= phi then |-_H

What is the definition of the provability (derivability) relation?

G |-_H phi is the proof of phi in system H with premises in G

What is the definition of the resolution inference rules? [3]

1. [l \lor rest_1] [\neg l \lor rest_2] / [rest_1 \lor rest_2] (Resolution)

2. Sound and complete (variable elimination) proof system for CNF

3. If phi unsatisfiable then there exists a proof of the empty clause {}

What is the abstract syntax of propositional logic?

Commandes clavier:

= tourner,

= avant/arrière,

= faire défiler

phi := a | \neg phi | (phi \and phi) with a \in AP and phi \in APForm

What is the set AP?

Commandes clavier:

= tourner,

= avant/arrière,

= faire défiler

Atomic propositions

What is syntactic sugar? [1+4]

Commandes clavier:

= tourner,

= avant/arrière,

= faire défiler

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?

Commandes clavier:

= tourner,

= avant/arrière,

= faire défiler

-- || ↔ → \or \and \neg || ++

What is the domain of propositional logic?

Commandes clavier:

= tourner,

= avant/arrière,

= faire défiler

B={0,1}

What are the interpretations of propositional logic? [4]

Commandes clavier:

= tourner,

= avant/arrière,

= faire défiler

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?

Commandes clavier:

= tourner,

= avant/arrière,

= faire défiler

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}?

Commandes clavier:

= tourner,

= avant/arrière,

= faire défiler

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]

Commandes clavier:

= tourner,

= avant/arrière,

= faire défiler

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]

Commandes clavier:

= tourner,

= avant/arrière,

= faire défiler

1. \alpha |= a iff \alpha(a) = true

2. \alpha |= \neg phi iff \alpha !|= phi

3. \alpha |= phi₁ \and phi₂ iff \alpha |= phi₁ and \alpha |= phi₂

4. \alpha |= phi₁ \or phi₂ iff \alpha |= phi₁ or \alpha |= phi₂

5. \alpha |= phi₁ → phi₂ iff \alpha |= phi₁ implies \alpha |= phi₂

6. \alpha |= phi₁ ↔ phi₂ iff \alpha |= phi₁ iff \alpha |= phi₂

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

1 / 43

Cartes-fiches

What is the definition of completeness? [2]

1. Are all “correct” conclusions from premises derived

2. If |= phi then |-_H

What is the definition of the provability (derivability) relation?

G |-_H phi is the proof of phi in system H with premises in G

What is the definition of the resolution inference rules? [3]

1. [l \lor rest_1] [\neg l \lor rest_2] / [rest_1 \lor rest_2] (Resolution)

2. Sound and complete (variable elimination) proof system for CNF

3. If phi unsatisfiable then there exists a proof of the empty clause {}

Étudier

SC Chapter 2 Propositional Logic

Créer ou copier des fichiers d'apprentissage

Cartes-fiches

Veuillez vous connecter

Google

Apple ID

Microsoft

Switch edu-ID

Edulog

Google

Apple ID

Microsoft

Switch edu-ID

Edulog