First Order Logic Tutorial
This is a tutorial on first order logic. Some examples assume some familiarity with OBJ. Suitable material can be found in the following:
  1. Algebraic Semantics of Imperative Programs, and
  2. Theorem Proving and Algebra.
Many details and notations are simplified or omitted in these tutorial pages; they are intended to convey the flavor of the mathematics to software practitioners. The above references also give much more complete information on first order logic.

The buttons on the bottom of the pages will help you navigate. The [Next] button takes you to the next page, the [Prev] button takes you to the previous page, the [Home] button takes you to this home page, and the [BHome] button takes you to the background information home page.

[Next] [BHome] [Links Home]
12 October 1996