The Complexity of AI Algorithms.
Abstract
This report contains the results of two efforts. Both efforts focused on the resolution algorithm which is particularly well suited for automation on computers, and is one of the leading mechanisms used in automatic theorem proving. It can also be used in the deductive engine of an expert system. The deductive engine is an important component of any expert system. The first effort examined the complexity of logic programming and showed that the logic programming problem is NP-hard. This result motivated us to look at preprocessing techniques that allow part of the time cost to be paid beforehand. Several preprocessing techniques we proposed that offer a decrease in time cost at the expense of storage. The second effort investigates the relationship between input and unit resolution for Horn clause systems. A measure of non-linearity is given for unit refutations and establish that this measure has no upper bound over the set of unit refutations. Keywords: Automatic theorem proving; Resolution principle; Unit resolution; Input resolution; Horn clauses; Complexity.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1987
- Accession Number
- ADA193494
Entities
People
- C. Heinbach
- C. R. Hartmann
- M. Ben-jacob
- O. Murphy
- P. K. Varshney
Organizations
- Syracuse University