In this chapter we review the syntax and semantics of many-sorted first-order logic, and the concept of substitutions in this logic. The presentation attempts to be as concise as possible, and the reader is referred to a standard text in logic, such as Gallier , for a more thorough presentation. Lloyd  or Apt  is the accepted introduction to the theory of logic programming. The reader is invited to skip this chapter if and until it is needed.
KeywordsFunction Symbol Atomic Formula Conjunctive Normal Form Predicate Symbol Horn Clause
Unable to display preview. Download preview PDF.