In this monograph we present proof methods which apply to the the Horn clause subset of first-order logic. Horn clause logic has many interpretations which are important in computer science. In the context of programming languages, a definite clause of the form A ← B 1,..., B n is viewed as a definition of the procedure A in terms of the subprocedures B 1 ,...,B n , and a negative clause of the form ← B 1,..., B n , is viewed as a sequence of procedure calls. Horn clause logic can also be given an interpretation which generalizes the relational database model. Unit ground clauses are viewed as relations, definite clauses as integrity constraints, and the class of negative clauses as the query language. This interpretation is a generalization of the standard relational model because it allows recursion among the relations, and has given rise to the idea of a deductive database .
KeywordsLogic Programming Operational Semantic Horn Clause Automate Theorem Prove Deductive Database
Unable to display preview. Download preview PDF.