Naval Weapons Laboratory, Dahlgren, Va.: NWL technical report TR. 2864. Role of theorem proving in artificial intelligence [-with list of references]; by Hartmut G. M. Huber.