Logic Flashcards
Syntax
Specifies all sentences are well formed
Sound
A inference algorithm that derives only entailed sentences is called sound or truth preserving
Completeness
An inference algorithm is complete if it can derive any sentence that is entailed
Logical entailment
The idea that sentence follows from another sentence. Formal definition of entailment : a is entailed by b iff every model in which a is true b is also true. Which means a is a subset of b
Semantics
Defines the truth of each sentence with respect to each possible world
Inference algorithm : model checking - propositional logic
Enumerate all the models and check if alpha is true in every model where kb is true which means kb must be a subset of alpha. The algorithm is sound because it directly implements the definition of entailment and complete because it works for all values of alpha and kb and always terminates as long as there are only finite models to enumerateTime complexity 2 power n. Space complexity is order of n because it is dfs. N is the number of symbols in kb and alpha
Inference algorithm : theorem proving - propositional logic
Take a sentence from the kb and apply the rules of inference I.e. Commutativity , associativity or double negation etc and derive the alpha we seek.
Logical equivalence
Two sentences a and b are equivalent if they are true in the same set of models. This means that a entails B and B entails a I.e. Whenever a is true b is true and whenever b is true a is true
Validity
A sentence is valid if it is true in all the models
Satisfiability
A sentence is true if it is true in or satisfied by some model. Enumerate all the models until you find one that satisfies the sentence
Inference rule : modus ponens
Whenever any sentence of the form a implies b and a are given we can infer sentence b
Difference between entailment and inference
Inference ( syntax )is how it is done while entailment is the real world. If inference is sound and complete we have an entailment ( semantics) : this was written based on prof answer
Model
Represents a state or a world
Dpll
Used to check for satisfiability. Takes a kb and alpha and checks if it exists in any models. Uses resolution rules like pure symbols and unit clauses
DPLL Algorithm
if CNF is empty then
return true
else if CNF contains an empty clause then
return false
else if CNF contains a pure literal x then
return DPLL(CNF(x))
else if CNF contains a unit clause {u} then
return DPLL(CNF(u))
else
choose a variable x that appears in CNF
if DPLL(CNF(x)) = true then return true
else return DPLL(CNF(¬x))
