Lógica F - F-logic

F-logic ( quadro lógico ) é uma representação do conhecimento e ontologia idioma . A lógica F combina as vantagens da modelagem conceitual com linguagens orientadas a objetos e baseadas em quadros e oferece uma sintaxe declarativa, compacta e simples, bem como a semântica bem definida de uma linguagem baseada em lógica.

Os recursos incluem, entre outros, identidade de objeto, objetos complexos, herança , polimorfismo , métodos de consulta, encapsulamento . A lógica F mantém a mesma relação com a programação orientada a objetos que o cálculo relacional clássico está com a programação de banco de dados relacional .

Visão geral

A lógica F foi desenvolvida por Michael Kifer na Stony Brook University e Georg Lausen na University of Mannheim . A lógica F foi originalmente desenvolvida para bancos de dados dedutivos, mas agora é mais frequentemente usada para tecnologias semânticas, especialmente a web semântica . A lógica F é considerada um dos formalismos para ontologias , mas a lógica de descrição (DL) é mais popular e aceita, assim como o OWL baseado em DL .

Um ambiente de desenvolvimento para lógica F foi desenvolvido no projeto NeOn e também é usado em uma variedade de aplicativos para integração de informações, resposta a perguntas e pesquisa semântica . Antes da versão 4 do editor de ontologias Protégé, o F-Logic era suportado como um dos dois tipos de ontologia.

A sintaxe de quadro do dialeto lógico básico do formato de intercâmbio de regra (RIF BLD) padronizado pelo World Wide Web Consortium é baseado na lógica F; O RIF BLD, entretanto, não inclui recursos de raciocínio não monotônicos da lógica F.

Em contraste com a descrição lógica baseada no formalismo de ontologia, a semântica da lógica F é normalmente aquela de uma suposição de mundo fechado em oposição à suposição de mundo aberto de DL . Além disso, a lógica F é geralmente indecidível , enquanto a lógica de descrição SHOIN na qual OWL DL se baseia é decidível. No entanto, é possível representar declarações mais expressivas na lógica F do que com as lógicas de descrição.

A descrição mais abrangente da lógica F foi publicada em 1995. O artigo preliminar de 1989 ganhou o prêmio Test of Time de 1999 da ACM SIGMOD . Um artigo subsequente de 1992 ganhou o Prêmio Teste do Tempo de 2002 da ACM SIGMOD.

Sintaxe da lógica F

As classes e os indivíduos podem ser definidos na lógica F da seguinte forma:

man::person.
woman::person.
brad:man.
angelina:woman.

Isso afirma que "homens e mulheres são pessoas" e que "Brad é um homem" e "Angelina é uma mulher".

As declarações sobre classes e indivíduos podem ser feitas da seguinte forma:

person[hasSon=>man].
brad[hasSon->{maddox,pax}].
married(brad,angelina).

Isso define que "o filho de uma pessoa é um homem", "Maddox e Pax são os filhos de Brad" e "Brad e Angelina são casados".

Além disso, é possível representar axiomas na lógica F da seguinte maneira:

man(X) <- person(X) AND NOT woman(X).
X:person[hasFather->Y] <- Y:man[hasSon -> X].

Isso significa "X é um homem se X é uma pessoa, mas não uma mulher" e "se X é filho de Y, então X é uma pessoa e Y é o pai de X".

O sistema Flora-2 introduziu uma série de mudanças na sintaxe da lógica F, tornando-a mais adequada para uma representação de conhecimento e sistema de raciocínio em oposição a apenas uma lógica teórica. Em particular, as variáveis ​​foram prefixadas com uma marca?, A distinção entre propriedades funcionais e multivaloradas foi descartada e substituída por restrições de cardinalidade, além de outras alterações importantes. Por exemplo, o par de frases acima é assim em Flora-2:

man(?X) <- person(?X) \and \naf woman(?X).
?X:person[hasFather->?Y] <- ?Y:man[hasSon -> ?X].

Aqui \ naf é a negação padrão ("naf" significa negação como falha com base na semântica bem fundada ); Flora-2 também suporta a chamada negação explícita, que está mais próxima da negação na lógica clássica.

Linguagens baseadas na lógica F

Referências