TY  - BOOK
AU  - Fitting,Melvin
TI  - First-order logic and automated theorem proving
T2  - Texts and monographs in computer science
SN  - 0387972331 (alk. paper)
U1  - 005.131 23
PY  - 1990///
CY  - New York
PB  - Springer-Verlag
KW  - Automated theorem proving
KW  - Symbolic and mathematical logic
KW  - Logic design
KW  - Artificial intelligence
N1  - Includes bibliographical references (p. [233]-236) and index; 1. Background--
2. Propositional logic--
3. Semantic tableaux and resolution--
4. Other propositional proof procedures--
5. First-order logic--
6. First-order proof procedures--
7. Implementing tableaux and resolution--
8. Equality--
References--
Index
N2  - A mathematical monograph on first-order logic. Applications to automated theorem-proving are considered and Prolog programmes provided. May serve as a first text on formal logic for graduate students of computer science or mathematics.
ER  -