Raciocínio automatizado

Raciocínio automatizado é uma sub-área da inteligência artificial que estuda formas de simular raciocínio lógico por meio de métodos computacionais.

Um dos principais algoritmos para raciocínio dedutivo automatizado, denominado SLD-resolução, usa refutação e apresenta as seguintes características:

– restringe-se à uma classe de fórmulas denominada cláusulas de Horn;

– emprega a resolução e unificação como regras de inferência;

– adota uma estratégia de busca em profundidade para controlar as inferências;

– introduz o conceito de predicado computável;

– introduz o conceito de negação por falha finita.