Notas do Capítulo 6
O capítulo 6 cobre algum material básico sobre lógica matemática e computacional. O conteúdo deste capítulo foi usado como notas para parte de um curso teórico de ciência da computação sobre raciocínio automatizado em nível de mestrado entre 1995 e 2001. Presumiu-se que o aluno tinha pelo menos um curso de formação em lógica, com pelo menos um introdução informal à lógica simbólica.
A seção 6.2 cobre a lógica positiva. Bases de regras e metas positivas são definidas. Os tópicos cobertos incluem o universo Herbrand para uma base de regra, substituições de respostas, interpretações e modelos, respostas, modelo mínimo, árvores de regras, computação Prolog e extração de provas como árvores de regras. O material desta seção é uma boa companhia para o material do popular livro Foundations of Logic Programming de J.W. Lloyd (1984,1987).
A Seção 6.3 desenvolve um bom tradutor do Prolog da lógica de primeira ordem para as regras da lógica da forma normal. As regras da forma normal servem como entradas para um programa de raciocínio da forma normal na seção 6.4.
A Seção 6.4 desenvolve um interpretador de consulta de base de regra normal interessante para lógica disjuntiva linear. A semântica para bases de regra normais é baseada em estados e árvores de regras. As árvores de regras foram introduzidas em uma configuração mais simples na Seção 6.2, para bases de regra positivas. O projeto e a implementação de um interpretador de consulta de base de regra normal são desenvolvidos no Prolog.
A Seção 6.5 discute algumas das questões relacionadas à integridade e integridade do interpretador de base de regra normal desenvolvido na Seção 6.4. O uso de um Tabeled Prolog (como o XSB Prolog) é discutido brevemente.
A Seção 6.6 apresenta uma ferramenta de visualização Java para exibir as árvores de regra geradas pelo interpretador de base de regra normal da Seção 6.4.
Recentemente (c. 2005), a lógica geométrica finitária (também conhecida como lógica coerente) parece ser uma alternativa interessante à lógica disjuntiva linear. Por favor, consulte Geolog and Skolem Machines para algumas notas da web com foco nas implementações Prolog de lógica geométrica.