Logic

We can use logic, along with a Knowledge Base, which consistents a set of sentences, in order to reason and draw conclusions.

Logical reasoning is gaurenteed to be correct if the available information is correct.

Duality of Logic states that given any true statement/tautalogy we are able to derive another tautalogy by interchanging OR and AND and True and False.

To define logic, we have a set of variables, sentences and operations. And we try to capture the semantics of the real world through a logical representation in our logical syntax.

If a sentence \(\alpha\) is true in model world \(m\), we say \(m\) satisfies \(\alpha\). \(M(\alpha)\) is the set of models of \(\alpha\)

\(\alpha\) entails \(\beta\) if whenever \(\alpha\) holds, \(\beta\) holds as well. This is the same thing as saying \(M(\alpha) \subset M(\beta)\).

We can check if a knowledge base entails something via model checking, simply enumerating all possible models to ensure \(M(KB) \subset M(\alpha)\).

We can use this property for logical inference. An inference algorithm that derives only entailed sentences is sound, or truth perserving. It is complete if the algorithm can derive derive any sentence that is entailed. Finally we must consider grounding or converting our logical syntax into real world semantics.

Propositional Logic

Propositional logic can be expressed as a set of operators, \(\neg, \land, \lor, \implies, \iff\).

We say that two sentences are logically equivalent if they are true in the same set of models.

\(\alpha\) is valid if it is true in every possible world.

\(\alpha\) is inconsistent if it is not true in every possible world. If a model is not inconsistent, it is satisfiable.

\(\alpha \models \beta\) if and only if \(\alpha \land \neg \beta\) is unsatisfiable.

\(\alpha\) and \(\beta\) are mutually exclusive if there are no worlds where both \(\alpha\) and \(\beta\) are true.

Inference Rules and Resolution

Modus Ponus - \(\alpha \implies \beta, \alpha\) infers \(\beta\)

And-Elimination - \(\alpha \land \beta\) infers \(\beta\) and \(\alpha\)

montonicity states that if \(KB \models \alpha\), then \(KB \land \beta \models \alpha\).

PL-Resolution(KB, a):
    clauses = KB $ !a
    for each pair of clauses, 
        resolvents = PL
        if resolvents contains the empty clause return true
        new =  new | resolvents
    if new is a subset of clauses return false
    clauses = clauses | new

Resolution is complete. To see this, we note define resolution closure to be the set of all clauses that our algorithm can derive. This set is finite, because there is a limited number of symbols to arrange. Hence our algorithm always terminates.

ground resolution theorem - If a set of clauses is unsatisfiable, then the resolution closure of those clauses contains the empty clause.

Forward chaining determines if a single proposition symbol, \(q\) is entailed by the knowledge base. Tries to reason from a knowledge base to a query.

function forward_chaining(KB, q)
count where count[c] is the number of symbols in c's premise
inferred where inferred[s] is initially false for all symbols
agenda =  queue of known true symbols in the KB

while agenda is not empty
    p = agenda.pop()
    if p = q then return true
    if inferred[p] = false
        inferred[p] = true
        for each clause c in KB where p is in c.premise
            decrement count[s]
            if count[c] = 0 then add c.conclusion to agenda.
return false

Backwards chaining tries to reason backwards from \(q\). If q is known, no work is needed. Otherwise, find all implications in the KB whose conclusio is q. If all the premises are true (proved via backward chaining) then q is true. This is an example of goal-directed reasoning.

Davis-Putnam-Logemann-Loveland

Algorithm for complete backtracking inference. Takes in a sentence in CNF form.

Early Termination - algorithm detects whether a sentence must be true or false even with a partially completed model.

Pure Symbol Heurestic - a symbol is pure if it always appears with the same sign in all clauses, makes it easier to assign.

Unit Caluse Heurestic - a clause with just one literal or a clause in which all literals except one are assigned false. Cascades via unit propogation.

DPLL-Satisfiable(s)
    clauses = set of clauses in the CNF representation of s
    symbols = set of propositional symbols in s
    return DPLL(clause, symbol, {})

DPLL(clauses, symbols, model)
    if every clause in clauses is true in model return True
    if some clause in clauses is false in model return False

    P, value = FindPureSymbol(symbols, clauses, model)
    if P return DPLL(clauses,symbols - P, model | P=value)

    P, value = FindUnitClause(clause, model)
    if P return DPLL(clauses,symbols - P, model | P=value)

    P = head(symbols), rest = rest(symbols)
    return DPLL(clauses, rest, model | P=true) or 
           DPLL(clauses, rest, model | P=false)

This can be used in conjunction with numerous tricks to speed up performance, namely component analysis, variable and value ordering, and intelligent backtracking, random restarts, and clever indexing.

We can also use local search to find a satisfiable equation. In general some SAT problems are underconstrained, that is they are likely to have a nearby solution. Emperically, we see that there is a threshold of clause/symbol at around 3. Beyond this number dramatically reduces the chance of a solution.

Converting to CNF

1. Eliminate \(\iff\) by replacing \(\alpha \iff \beta\) with \((\alpha \implies \beta) \land (\beta \implies \alpha)\)
2. Eliminate \(\implies\) by replacing \(\alpha \implies \beta\) with \(\neg \alpha \lor \beta\)
3. Remove \(\neg\) outside of liters via double-negation elimination and DeMorgan’s Law.
4. Distribute \(\lor\) over \(\land\) whenever possible.

First-order Logic

First order logic exhibits compositionality, which means that the meaning of a sentnec is a function of the meaning of its parts.Predicate, or first order logic contains a predicate \(p(x)\) that evaluates to T/F.

Models for first-order logic have objects in them. The domain of a model is the set of objects it contains. Objects may be related (represented by a set of tuples). Consists of constant symbols, predicate symbols, function symbols.

A term is a logical expression that refers to an object.

Existential qualifier - \(\exists x [p(x)]\) there exists an \(x\) such that \(p(x)\) is true. Use \(\implies\).

Universal qualifier - \(\forall x [p(x)]\) \(p(x)\) is true for all \(x\). Use \(\land\).

Quantifiers are related to each other in the following way: \(\neg(\forall x [p(x)]) = \exists x [\neg p(x)]\)

We either use a quantifier or instantiate the predicate to turn it to T/F.

If we make the unique-names assumption (every object has a distinct name), the closed-world assumption (atomic scentence not known to be true are false), and domain closure (each model contains no more domain element than those named by constant symbols) we recieve a database language.

First-Order Reasoning

Inference Rules

Universal Instantiation - subsitute a ground term for the variable.

Existential Instantiation - subsitute a Skolem constant for the variable.

This technique of propositionalization can be made completely general, since any sentence sentence entailed by the original knowledge base can be proved with a finite subset of the knowledge base. In general, the question of entailment for first order logic is semidecidable.

Generalized Modus Ponens - for atomix sentences \(p_i, p_i', q\) where this a subsitution \(SUB(\theta, p_i') = SUB(\theta, p_i)\) for all \(i\).

Lifted inference rules require finding subsitutions, called unifications to make different logical expressions look identitical.

\(Unify(p, q) = \theta\) where \(SUB(\theta, p) = SUB(\theta, q)\)

In this case, we need to standardize apart the two sentences being unified, which means renaming variables. In general, there is a single most general unifier that is unique up to renaming and subistuting variables. To check unifiers, we occur check,which ensures that no variable itself occurs inside the term. \(S(x)\) can’t unify with \(S(S(x))\).

Resolution

1. Eliminate implications
2. Move \(\neg\) inwards
3. Standardize variables - change variables so that the same variable is not used twice
4. Skolemize - remove any existential quantifiers via Skolemization constants/function
5. Drop universal quantifiers
6. Distribute \(\lor\) over \(\land\)

Resolution inference is simply a lifted version of normal resolution. Two clauses can be resolved if one unifies with the negation of the other. This is binary resolution. We also need factoring, the removal of redundant ordering to get a complete solution.

However, resolution can give us nonconstructive proofs. We can combat this to add a special answer literal to the negated goal.

Resolution in general is refutation complete* - that is if a a set is sentences is unsatisfiable, then resolution will be able to derive a contradiction. It cannot be used to generate all logical consequences of a set of sentences, but it can be used to establish a given sentence is entailed.

1. If \(S\) is unsatisfiable, then there exists a particular set of ground instances such that this set is also unsatisfiable
2. Propositional resolution is complete for ground instances
3. Any propositionl resolution proof for fround sentences can be formulated into a first order resolution proof.

Finite number of literals anyways, so finite runtime. Godels Incompletness Theorem states that there are true statements that we are unable to prove.