Consequência Lógica em LPO

Definição: Satisfação/Entailment/Consequência Lógica

Dada uma interpretação $\mathfrak{I}$ e uma lookup table $\mu$, dizemos que uma fórmula $\alpha$ é satisfeita na interpretação $\mathfrak{I}$ (e que escrevemos como $\mathfrak{I},\mu \models \alpha$ segundo Levesque, e $\mathfrak{I}{\models }_{\mu }\alpha$ segundo Huth) de acordo com as seguintes fórmulas:

• Dados termos $(t_1,\dots ,t_n)$ e predicado $n$-ário $P$, então

$$\mathfrak{I},\mu \models P(t_1,\dots ,t_n)⟺(\Vert t_1\Vert ,\dots ,\Vert t_n\Vert )\in \mathcal{I}[P]$$

• $\mathfrak{I},\mu \models (t_1=t_2)⟺\Vert t_1{\Vert }_{\mathfrak{I},\mu }=\Vert t_2{\Vert }_{\mathfrak{I},\mu }(\in D)$
• $\mathfrak{I},\mu \models \neg \alpha ⟺$ it’s false that $\mathfrak{I},\mu \models \alpha$;
• $\mathfrak{I},\mu \models (\alpha \wedge \beta )⟺$ $\mathfrak{I},\mu \models \alpha$ e $\mathfrak{I},\mu \models \beta$
• $\mathfrak{I},\mu \models (\alpha \vee \beta )⟺$ $\mathfrak{I},\mu \models \alpha$ ou $\mathfrak{I},\mu \models \beta$
• $\mathfrak{I},\mu \models \exists x.\alpha ⟺\exists {\mu }^{\prime }\mid \mathfrak{I},{\mu }^{\prime }\models \alpha$ para alguma lookup table que difira de $\mu$ em no máximo $x$
• $\mathfrak{I},\mu \models \forall x.\alpha ⟺\forall {\mu }^{\prime }\mid \mathfrak{I},{\mu }^{\prime }\models \alpha$ para qualquer lookup table que difira de $\mu$ em no máximo $x$

Como sentenças $\alpha$ são fórmulas sem variáveis livres, elas são invariantes a variable assignments $\mu$. Por isso, escrevemos que

$$\mathfrak{I}\models \alpha$$

quando quisermos dizer que $\alpha$ é verdadeiro sob a interpretação $\mathfrak{I}$, e que é falso caso contrário. São as sentenças que serão as unidades de conhecimento em uma base de conhecimento.

Referências

• BRACHMAN, Ronald J.; LEVESQUE, Hector J.; REITER, Raymond (Ed.). Knowledge representation. MIT press, 1992.
• HUTH, Michael; RYAN, Mark. Logic in Computer Science: Modelling and reasoning about systems. Cambridge university press, 2004.