Consequência Lógica em LPO

up:: 025 MOC Lógica de Primeira Ordem

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

Dada uma interpretação e uma lookup table , dizemos que uma fórmula é satisfeita na interpretação (e que escrevemos como segundo Levesque, e segundo Huth) de acordo com as seguintes fórmulas:

• Dados termos e predicado -ário , então

• it’s false that ;
• e
• ou
• para alguma lookup table que difira de em no máximo
• para qualquer lookup table que difira de em no máximo

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

quando quisermos dizer que é verdadeiro sob a interpretação , 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.