Propositional Logic

Entailment, derivation

$KB=\{\phi_1, ..., \phi_n\}$

$KB \models \psi$, or $KB$ entails $\psi$ $\iff$ every model of $KB$ is a model of $\psi$. To check entailment we need to check that $KB \cup \{\neg \psi\}$ is unsatisfiable, which means that we can derive false from it:

$$KB \cup \{\neg \psi\} \models \bot$$

$KB \vdash \psi$, or $\psi$ is derived from $KB$ $\iff$ $\psi$ can be obtained from $KB$ via an inference algorithm. To check derivation we need to use calculus rules.

Given $KB$ and $\psi$, assess if $KB \models \psi$. This is done via model checking, which is just a check performed with truth tables or via DPLL. A different approach is logic inference theorem proving (synctactical proof), which works by applying inference rules.

DPLL Algorithm

Model checking via backtracking search algorithm. It uses CNF formulas representation, in particular we start by looking for pure symbols, that are symbols for which the following constraint holds true: . A pure symbol can be assumed to be true when applying DPLL. If for example we have $eg R$ in our domain, then we can assume that $R=\bot$ .

Even simpler the case in which we have unit clauses, which are clauses which are made up of just one literal. We start simplifying clauses from them, and then we continue by reducing clauses to pure clauses by applying FOL rules.

If we do not have neither pure symbols, nor unit clauses, we need to try some possible values. This is done by branching, which consists of assuming that a symbol has a certain value, and checking if we can find a valuation that is true for all formulas. If we find at least a false, then we need to try another branch, until we try every possible value (true or false) for every possible symbol.

Resolution calculus

Resolution is similar to DPLL (when this is used to establish entailment): it starts from a CNF representation of the premises and the negation of the conclusion.

Forward chaining

Considers definite clauses and applies Modus Ponens to generate new facts:

MP: and , infer $Y$.

Graphical example:


Backward chaining

Same, but in reverse (we start building the graph from the top, which is the goal). Example: