Prolog Programming Based on Predicate Logic

Horn logic in first order predicate logic is the theoretical basis of artificial intelligence program language Prolog.The use of Prolog in computer can implement mechanization.This causes the problem of automatic solving and theorem proof to be viable.The paper starts with an introduction to the theoretical foundations of Horn logic and the basic principles of Prolog.Then in the next part of the paper the principles of Horn clause,SLD resolution,searching and backtracking are used to discuss how to carry out some applications of automatic inferences in computer,such as mathematical function and theorem proving.