Propositional Logic
90 flashcards · Other · by Martin Gegenbauer
In propositional logic, we are interested in declarative sentences that can be true or false.
In propositional logic, we are interested in declarative sentences that can be true or false.
Write the following sentence in propositional logic: If it is hot and humid, then it will rain.
(hot ∧ humid) ⇒ will_rain
Write the following sentence in propositional logic: If it is humid, then it is hot.
humid ⇒ hot
Write the following sentence in propositional logic: It rains, and when it rains, there are clouds.
rains ∧ (rains ⇒ cloudy)
Write the following sentence in propositional logic: If it rains then there are clouds, but now it is not cloudy.
(rains ⇒ cloudy) ∧ ¬cloudy
Write the following sentence in propositional logic: It rains only if it is cloudy, but now it does not rain.
(rains ⇒ cloudy) ∧ ¬rains
A proposition is a statement that can be either true or false. It must be one of them, and it cannot be both. Examples of propositions: It rains. Albert Einstein was a Greek philosopher. Examples which are not propositions: 1 + 2 Beauty and the Beast
A proposition is a statement that can be either true or false. It must be one of them, and it cannot be both. Examples of propositions: It rains. Albert Einstein was a Greek philosopher. Examples which are not propositions: 1 + 2 Beauty and the Beast
In logic, syntax is anything related to formal languages or formal systems, without regard to any interpretation or meaning given to them. Syntax is concerned with the rules used for constructing, or transforming the symbols and words of a language, as contrasted with the semantics of a language concerned with its meaning.
In logic, syntax is anything related to formal languages or formal systems, without regard to any interpretation or meaning given to them. Syntax is concerned with the rules used for constructing, or transforming the symbols and words of a language, as contrasted with the semantics of a language concerned with its meaning.
Propositional alphabet Definition An alphabet of propositional logic consists of three disjoint sets of symbols: propositional variables P\mathcal{P}P , propositional constants { ⊥\bot⊥ , ⊤\top⊤ }, logical connectives {¬, ∧, ∨, ⇒, ⇔}. It is assumed that P\mathcal{P}P is countably infinite. Letters p,q,r,s,l,wp, q, r, s, l, wp,q,r,s,l,w (maybe with subscripts) will be used to denote the elements of P\mathcal PP . Sometimes, more intuitive names are also used, e.g. rainsrainsrains or cloudycloudy…
Propositional alphabet Definition An alphabet of propositional logic consists of three disjoint sets of symbols: propositional variables P\mathcal{P}P , propositional constants { ⊥\bot⊥ , ⊤\top⊤ }, logical connectives {¬, ∧, ∨, ⇒, ⇔}. It is assumed that P\mathcal{P}P is countably infinite. Letters p,q,r,s,l,wp, q, r, s, l, wp,q,r,s,l,w (maybe with subscripts) will be used to denote the elements of P\mathcal PP . Sometimes, more intuitive names are also used, e.g. rainsrainsrains or cloudycloudy…
Propositional formulas Definition Formulas of propositional logic are defined by the grammar: F::=F ::=F::= ⊥\bot⊥ | ⊤\top⊤ | ppp | (¬F)(\neg F)(¬F) | (F1∧F2)(F_1 \land F_2)(F1∧F2) | (F1∨F2)(F_1 \lor F_2)(F1∨F2) | (F1⇒F2)(F_1 \Rightarrow F_2)(F1⇒F2) | (F1⇔F2)(F_1 \Leftrightarrow F_2)(F1⇔F2) ⊥,⊤\bot, \top⊥,⊤ , and ppp are called atoms, or atomic formulas. The others are compound formulas. If p,q,r∈Pp, q, r \in \mathcal{P}p,q,r∈P , then the following expressions are formulas: ((p∧q)⇒r),(p…
Propositional formulas Definition Formulas of propositional logic are defined by the grammar: F::=F ::=F::= ⊥\bot⊥ | ⊤\top⊤ | ppp | (¬F)(\neg F)(¬F) | (F1∧F2)(F_1 \land F_2)(F1∧F2) | (F1∨F2)(F_1 \lor F_2)(F1∨F2) | (F1⇒F2)(F_1 \Rightarrow F_2)(F1⇒F2) | (F1⇔F2)(F_1 \Leftrightarrow F_2)(F1⇔F2) ⊥,⊤\bot, \top⊥,⊤ , and ppp are called atoms, or atomic formulas. The others are compound formulas. If p,q,r∈Pp, q, r \in \mathcal{P}p,q,r∈P , then the following expressions are formulas: ((p∧q)⇒r),(p…
Semantics in logic is concerned with the meaning of a sentence.
Semantics in logic is concerned with the meaning of a sentence.
In propositional logic, there are two truth values, true and false. Let B:={true,false}\mathbb{B} := \{true, false\}B:={true,false} : the set of truth values.
In propositional logic, there are two truth values, true and false. Let B:={true,false}\mathbb{B} := \{true, false\}B:={true,false} : the set of truth values.
Semantics of connectives
Semantics of connectives
Boolean valuations A boolean valuation (or, simply, a valuation, also called an assignment) is a function v:P→Bv : P → \mathbb{B}v:P→B from propositional variables to truth values. The semantics of a propositional formula FFF depends on the valuation of the propositional variables that occur in FFF .
Boolean valuations A boolean valuation (or, simply, a valuation, also called an assignment) is a function v:P→Bv : P → \mathbb{B}v:P→B from propositional variables to truth values. The semantics of a propositional formula FFF depends on the valuation of the propositional variables that occur in FFF .
Interpretation
Interpretation
Semantics of formulas The semantics of a formula FFF is given by truth tables. If FFF contains nnn propositional variables, then the truth table for FFF is of size 2n The truth table for ¬(p∧¬q)⇒r\neg(p \land \neg q) \Rightarrow r¬(p∧¬q)⇒r . (including its subformulas)
Semantics of formulas The semantics of a formula FFF is given by truth tables. If FFF contains nnn propositional variables, then the truth table for FFF is of size 2n2^n2n . The truth table for ¬(p∧¬q)⇒r\neg(p \land \neg q) \Rightarrow r¬(p∧¬q)⇒r . (including its subformulas)
Semantic notions A formula FFF is called: valid if [F]v=true[F]_v = true[F]v=true for all valuations vvv , satisfiable if [F]v=true[F]_v = true[F]v=true for some valuations vvv , unsatisfiable if [F]v=false[F]_v = false[F]v=false for all valuations vvv , refutable if [F]v=false[F]_v = false[F]v=false for some valuations vvv . A valuation vvv is called a model of a formula FFF , if [F]v=true[F]_v = true[F]v=true .
Semantic notions A formula FFF is called: valid if [F]v=true[F]_v = true[F]v=true for all valuations vvv , satisfiable if [F]v=true[F]_v = true[F]v=true for some valuations vvv , unsatisfiable if [F]v=false[F]_v = false[F]v=false for all valuations vvv , refutable if [F]v=false[F]_v = false[F]v=false for some valuations vvv . A valuation vvv is called a model of a formula FFF , if [F]v=true[F]_v = true[F]v=true .
Semantic notions Observations F is valid iff ¬F is unsatisfiable. F is unsatisfiable iff ¬F is valid. Every valid formula is satisfiable, but not vice versa. Every unsatisfiable formula is refutable, but not vice versa. The negation of a satisfiable formula is refutable and vice versa. F is a satisfiable refutable formula iff also ¬F is.
Semantic notions Observations F is valid iff ¬F is unsatisfiable. F is unsatisfiable iff ¬F is valid. Every valid formula is satisfiable, but not vice versa. Every unsatisfiable formula is refutable, but not vice versa. The negation of a satisfiable formula is refutable and vice versa. F is a satisfiable refutable formula iff also ¬F is.
A note on the translation The usual way of translating natural language phrases into logic: FFF or GGG : F∨GF \lor GF∨G FFF and GGG : F∧GF \land GF∧G If FFF then GGG : F⇒GF \Rightarrow GF⇒G FFF is sufficient for GGG : F⇒GF \Rightarrow GF⇒G FFF is necessary for GGG : G⇒FG \Rightarrow FG⇒F FFF is necessary for GGG and FFF is not sufficient for GGG : (G⇒F)∧¬(F⇒G)(G \Rightarrow F) \land \neg(F \Rightarrow G)(G⇒F)∧¬(F⇒G) FFF is necessary and sufficient for GGG : F⇔GF \Leftrightarrow GF⇔G FFF wheneve…
A note on the translation The usual way of translating natural language phrases into logic: FFF or GGG : F∨GF \lor GF∨G FFF and GGG : F∧GF \land GF∧G If FFF then GGG : F⇒GF \Rightarrow GF⇒G FFF is sufficient for GGG : F⇒GF \Rightarrow GF⇒G FFF is necessary for GGG : G⇒FG \Rightarrow FG⇒F FFF is necessary for GGG and FFF is not sufficient for GGG : (G⇒F)∧¬(F⇒G)(G \Rightarrow F) \land \neg(F \Rightarrow G)(G⇒F)∧¬(F⇒G) FFF is necessary and sufficient for GGG : F⇔GF \Leftrightarrow GF⇔G FFF wheneve…
Translate this sentence into propositional logic and use and exclusive or for it: Tomorrow, I will stay the whole day at home or go to visit my friend.
The translation into propositional logic: (stay_home ∨ visit_friend) ∧ ¬(stay_home ∧ visit_friend)
Translate this sentence into propositional logic and derive your own propositional variables: For walking on the path to be safe, it is necessary but not sufficient that berries not be ripe along the path and for rabbits not to have been seen in the area.
The translation into propositional logic: r : Rabbits have been seen in the area. b : Berries are ripe along the path. w : Walking on the path is safe. (w ⇒ (¬b ∧ ¬r)) ∧ ¬((¬b ∧ ¬r) ⇒ w)
FFF is a logical consequence of GGG , written G⊨FG \models FG⊨F : for all valuations vvv , if [G]v=true[G]_v = true[G]v=true , then [F]v=true[F]_v = true[F]v=true .
FFF is a logical consequence of GGG , written G⊨FG \models FG⊨F : for all valuations vvv , if [G]v=true[G]_v = true[G]v=true , then [F]v=true[F]_v = true[F]v=true . Those are synonyms: logical consequence – semantic consequence G⊨FG \models FG⊨F – G entails F
FFF and GGG are logically equivalent, written F≡GF \equiv GF≡G : for all valuations vvv , [F]v=[G]v[F]_v = [G]_v[F]v=[G]v .
FFF and GGG are logically equivalent, written F≡GF \equiv GF≡G : for all valuations vvv , [F]v=[G]v[F]_v = [G]_v[F]v=[G]v . Those are synonyms: logically equivalent – semantically equivalent
What is the logical equivalent of this?
What is the logical equivalent of this?
What is the logical equivalent of this?
What is the logical equivalent of this?
What is the logical equivalent of this?
What is the logical equivalent of this?
What are the logical equivalents of those?
What is the logical equivalent of this?
What are the logical equivalents of those?
What are the logical equivalents of those?
What are the logical equivalents of those?
What are the logical equivalents of those?
What are the logical equivalents of those?
What are the logical equivalents of those?
What is a literal?
Literal: a propositional variable or its negation.
What is negation normal form (NNF)?
What is conjunctive normal form (CNF)?
What is disjunctive normal form (DNF)?
How can a formula be transformed into NNF?
How can a formula be transformed into CNF or DNF?
What is the complexity of a NNF transformation?
What is the complexity of a CNF or DNF transformation?
When are two formulas F and G equisatisfiable?
How can we avoid the exponential blowup of the CNF or DNF transformation?
What is the key idea of Tseitin transformation?
What is the logical equivalence of this formula?
What is the logical equivalence of this formula?
What is the logical equivalence of this formula?
What is the logical equivalence of this formula?
What is the logical equivalence of this formula?
Apply Tseitin transformation to
What are the properties of Tseitin transformation?
Is propositional logic decidable?
Yes. Propositional logic is decidable.
For any formula in propositional logic, can we find out whether it is satisfiable or unsatisfiable, refutable or valid?
Yes, we can.
What is the main drawback of a truth table?
It is inefficient.
What are the equivalent formulations of those problems?
Name three proof methods in propositional logic.
What is the goal of a propositional inference system?
What is the key idea of the resolution method?
What is the complement of a literal?
What is the resolvent of two clauses, and what are the parents of a resolvent?
When does the performance of the resolution don't make sense?
Resolvent = Res(), Clause 1 = C1C_1C1 , etc. Res( C1,C2C_1, C_2C1,C2 ) is satisfiable iff { C1,C2C_1, C_2C1,C2 } is satisfiable.
Resolvent = Res(), Clause 1 = C1C_1C1 , etc.
Explain the resolution procedure!
What is a semantic tree?
What is a failure node in a semantic tree?
What is an inference node in a semantic tree?
Do inference nodes in a semantic tree always turn into failure nodes?
If Ψ\PsiΨ is unsatisfiable, then RESOLUTION( Ψ\PsiΨ ) returns Unsat.
If Ψ\PsiΨ is unsatisfiable, then RESOLUTION( Ψ\PsiΨ ) returns Unsat.
What is sequent calculus? What is a sequent in sequent calculus? What is the antecedent of the sequent? What is the consequent of the sequent?
Which three forms of inference rules do you know in sequent calculus?
What is the Gentzen System in sequent calculus?
How do we prove in sequent calculus?
What is the idea behind the semantic tableaux?
What are α\alphaα - and β\betaβ -formulas in the context of semantic tableaux?
What are the tableaux expansion rules?
Which steps are taken in the semantic tableau construction procedure?
Which kinds of tableaux do exist?
What can be said about the termination of the tableau construction?
What can be said about the soundness of the tableau construction?
What is a Hintikka set?
What can be said about the completeness of the tableau construction?
How can a semantic tableau be proven?
How can the efficiency of a semantic tableau be improved?
What is an analytic tableaux?
A semantic tableau of a formula is closed if the formula is unsatisfiable and open if it is satisfiable.
A semantic tableau of a formula is closed if the formula is unsatisfiable and open if it is satisfiable.