Entailment vs Inference KB entails alpha means that if the KB is true then so must alpha. KB |- alpha (i.e. alpha can be infered from KB) just means that with some inference procedure we can derive alpha. The difference between entailment and inference is that inference procedures cannot necessarily find everything that can be entailed and inference procedures are not necessarily correct/sound (i.e. can derive things that aren't necessarily true).
First Order-Logic
Predicate(Arguments) relations sentence
Universal Instantiation
这里的替换只能用ground term
Existential instantiation
给一个存在形式的sentence，通过替换constant（其他地方没有被用过）可以infer new sentence
Unification vs pattern matching
Unification:allows variables on both sides
Pattern Matching:allows variables on only one side
Forward chaining
从下到上
Backward chaining
Logic programming
A ∧ B ⇒ C in Prolog we have C :- A, B.
The notation [E|L] denotes a list whose first element is E and whose rest is L.
append([A|X],Y,[A|Z]) :- append(X,Y,Z).
[A|Z] is the result of appending [A|X] onto Y, provided that Z is the result of appending X onto Y
CNF conversion
- Eliminate implications
- Move ¬ inward
- Standardize variables
Where the same variable name is used across different quantifiers, change the name of one of them to something unique. - Skolemization
Skolemization is the process of removing existential quantifiers by elimination.
把存在形式的都换掉 - Drop Universal quantifiers
- Distribute ⋁ over ⋀
- FOL/Propositional inference: forward backward resolution 三种，forward是通过现有的尝试推出结论，backward是从结论尝试反推，resolution是通过将逆命题加入KB然后推出空集（反证）；后者用modus ponens 比较多
- FOL/Propositional Logic CNF: 前者有任意存在 需要用sklome,后者直接转换即可
- Syntax: formal structure of sentences
- Semantics: truth of sentences with respect to models
- Model: A possible world that defines truth values for all sentences Entailment: necessary truth of one sentence given
another - Inference: determine whether sentence entailed by KB,Or equivalently, derive new sentences from old
- Soundness: produce only entailed sentences
- Completeness: can produce all entailed sentences Equivalence: sentences are true in the same models Validity: sentence is true in all models
- Satisfiability: sentence is true in some model
