logic

Question 1

what is a BNF (Backus Naur Form) and terminal and non-terminal symbols?

Answer 1

BNF looks like this:
lhs ::= rhs₁ |. . .| rhsₙ
where the lhs is a non-terminal symbol (expands into a rhs) and each rhs is either a terminal or non-terminal symbol

Question 2

what does arity and fixity of a terminal symbol mean?

Answer 2

arity: how many arguments thee symbol takes
fixity: where the symbol is placed in relation to the arguments. either prefix, infix or postfix meaning before, between and after the symbols

Question 3

what is a metavariable/ schematic variable?

Answer 3

a non-terminal symbol that can be used for general rules but represents an unknown value

Question 4

what is an axiom schemata?

Answer 4

a general rule that is accepted for all values of a schematic variable such as:
exp+0=exp. this rule with any value for exp is an axiom but as it is true for any exp, it is an axiom schemata

Question 5

what is the notation for substituting values into an equation?

Answer 5

(eq)[exp1\val1,exp2\val2,…]
example:
(exp+0=exp)[exp\1] outputs 1+0=1

Question 6

what is propositional logic?

Answer 6

a symbolic logic FORMAL LANGUAGE made of atomic propositions (true/ false propositions) and logical connectives(and, or, not, implication). syntax is
P ::= a | P ^P | P ∨P | P → P | ¬P with two special atoms (⊤,⊥)

Question 7

what is the scope of a connective and main connective of the formula?

Answer 7

scope of a connective: the connective and what it connects
main connective: the connective whose scope is the whole formula

Question 8

what are the 8 (10) inference rules of constructive natural deduction for propositional logic?

Answer 8

check here
https://canvas.bham.ac.uk/courses/65481/files/13872848?wrap=1

Question 9

what is the notation for saying that assuming conditions, something is true?

Answer 9

condition1, condition2, … , ⊢ proven statement
example:
P, P→Q ⊢ Q

Question 10

what is constructive/ intuitionistic and classical natural deduction?

Answer 10

both are proof theories that together with propositional logic (the formal language) make up a formal proof. they are both a collection of inference rules such as and-implication, negation-elimination etc. classical ND uses
double negation elimination (DNE): ¬¬A ⊢ A
law of excluded middle (LEM): ⊢ A∨¬A

Question 11

how do semantics work in propositional logic?

Answer 11

semantics means giving meaning to variables with the syntax φ(A) = T, φ(B) = F

Question 12

what is conjunctive/ disjunctive normal form?

Answer 12

CNF: formulas in the form (P∨P∨…)^(P∨P∨…)^…
DNF: formulas in the form (P^P^…)∨(P^P^…)∨…
where P is a literal meaning an atom or a negation of an atom
every proposition can be expressed in either form rearranging using proven equivalences

Question 13

what does valid, unsatisfiable, satisfiable, falsifiable and provable mean?

Answer 13

A is valid if φ(A) = T for all possible valuations φ of atoms in A.
A is unsatisfiable if φ(A) = F for all possible valuations φ of atoms in A.
A is satisfiable if there exists a valuation φ on atomic propositions such that φ(A) = T.
A is falsifiable if there exists a valuation φ on atomic propositions such that φ(A) = F.
provable: a formula can be proven with the natural deduction system. written like ⊢A

Question 14

how would you write that a formula is provable/ valid given premises?

Answer 14

provable: P₁, P₂, … , Pₙ ⊢ C meaning that the conclusion is always T for
(semantically) valid: P₁, P₂, … , Pₙ ⊨ C meaning that if all the premises are true, the conclusion is too. can always be proven using truth tables
with no premises: ⊢A and ⊨B

Question 15

what does soundness and completeness of a deduction system w.r.t a semantics system mean?

Answer 15

soundness: if ⊢A then ⊨A (if a formula is provable, it is valid)
completeness: if ⊨A then ⊢A (if a formula is valid, it is provable)
natural deduction is both sound and complete w.r.t truth table semantics

Question 16

how do you turn a proposition into DNF or CNF?

Answer 16

put proposition into a truth table
DNF: string together with an OR the clauses that make up every row where the conclusion is T
CNF: do the same as DNF but where the rows are F and string together the negation of the clauses with AND. then rearrange the formula with De Morgan’s law.

Question 17

what does N and NP mean

Answer 17

N is the class of problems that are solvable in polynomial time
NP is the class of problems that can be verified in polynomial time
N⊆NP

Question 18

what is SAT?

Answer 18

SAT is CNF satisfiability which is in NP

Question 19

what is the DPLL algorithm that is used in most SAT solvers?

Answer 19

sets an atom to either T or F. if T, remove all clauses containing the atom and remove all instances of the negation of the atom from remaining clauses. if F, remove all clauses containing the negation of the atom and remove all instances of the atom from remaining clauses. keep doing this until all clauses are gone (solvable). if a clause remains that is empty, backtrack and change the value of the last atom. if all combinations are tried, it is unsolvable.

Question 20

what is the precedence and associativity of the propositional logic symbols?

Answer 20

precedence (most to least): ¬, ^, ∨, →
associativity: all are right associative i.e. A^B^C = A^(B^C)

Question 21

what is included in predicate logic?

Answer 21

a type of symbolic logic that includes predicate logic but also has:
a domain: a non-empty set of objects to reason about such as N
variables: such as x,y,z that represent yet unknown members of the domain
predicates: true/false statement about objects such as even may be p(x)
quantifiers: universal quantifier ∀x. (for all x in the domain), existential quantifier ∃x. (there exists an x such that). quantifiers have highest precedence
functions: f(x,y,…) that output another object in the domain such as adding them
constants: arity 0 functions that output one object such as ‘a’ may be 0

Question 22

what is the scope of a quantifier?

Answer 22

the scope is the range where the quantifier acts over which in the case of predicate logic is everything to the right of the quantifier

Question 23

what are the 4 additional rules of predicate logic involving the quantifiers?

Answer 23

check here
https://canvas.bham.ac.uk/courses/65481/pages/week-9-materials-3?module_item_id=2858488

Question 24

what is the notation for substituting variables in a proposition?

Answer 24

P[x\y] substitutes all occurrences of x in the proposition P with y

Question 25

how do we write a predicate (relation) and function of arity n on domain D in predicate logic?

Answer 25

Rₚ ⊆ Dⁿ
Ff ∈ Dⁿ→D

Question 26

what is an example of a signature, model and a variable valuation?

Answer 26

signature: «zero, succ, add>,<even, odd»
model assigns meaning (semantics):{<0>,<2>,<4>,…}<N,«0, <n>→n+1, <n,m>→n+m>,<{n|even},{n|odd}>>>
variable valuation: x₁ → d₁, x₂ → d₂,...</n>

Question 27

what is the notation for assigning meaning to terms and formulas w.r.t the domain D,
the model M and the variable valuation v?

Answer 27

[[t]]ᵥᴹ takes a term from the signature and outputs the respective term in the model or takes a variable and returns its meaning
⊨ M,v,P outputs the predicate with all terms given meaning

Question 28

how do you give meaning to each type of formula in predicate logic?
example: ⊨ M,v P→Q iff ⊨ M,v Q whenever ⊨ M,v P

Answer 28

check here page 15:
https://canvas.bham.ac.uk/courses/65481/pages/week-9-materials-3?module_item_id=2858488

Question 29

what does it mean for a formula in predicate logic to be:
true
satisfiable
valid

Answer 29

true: P is true in the model M if ⊨M P
satisfiable: P is satisfiable if there exists a model that makes P true
valid: P is valid if it is true for all models M

Question 30

what are the three rules that introduce a new hypothesis?

Answer 30

implication introduction, negation introduction, existential quantifier elimination