Skip to main content

Review Logic Terminology

Review​

Propositional logic​

does not have predicates, just formulas of singular propositional symbols
ex: ¬𝑝 ∨ π‘ž β†’ r

First-order logic​

formulas use variables, constants, predicates, functions, βˆƒ, βˆ€

Variable​

generally end of alphabet: w, x, y, z

Constant​

generally start of alphabet: a, b, c, d

Predicate​

  • a property or relation
  • P(a) would mean a constant a has property P
  • P(x) would mean the same for indeterminate variable

Function​

  • constants are a subset of these with no parameters
  • generally f, g, h,...
  • maps within domain of variables f(x) -> y

Names​

Disjunction: V
Conjunction: ∧
Negation: Β¬

Conjunctive Normal Form (CNF)​

a set of clauses changed to a form where it becomes a conjunction of clauses where each clause is a disjunction of literals
¬ 𝐡 ∨ 𝐢 becomes (¬𝐡) ∧ (¬𝐢)
(A ∧ 𝐡) ∨ 𝐢 becomes (𝐴 ∨ 𝐢) ∧ (𝐡 ∨ 𝐢)

Unification​

attempt to find the most general unifier (mgu)
mgu is a valid mapping of variable/constant/function mapping to make two terms the same

Ex. if I have f(a) and f(x)
β€’ mgu mapping x->a makes f(a)=f(a)

Resolution​

Chα»©ng minh phαΊ£n chα»©ng

  1. Negate the conclusion trying to be proven(!)
  2. Then turn this into CNF
  3. Attempt to derive empty clause
  4. If found this indicates the set of clauses was not satisfiable
  5. This then means that the original conclusion was supported by the clauses