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 [23].


Logic Programming Operational Semantic Horn Clause Automate Theorem Prove Deductive Database 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 1990

Authors and Affiliations

  • Stan Raatz
    • 1
  1. 1.Department of Computer ScienceRutgers UniversityNew BrunswickUSA

Personalised recommendations