Inference and Decision Mechanisms in Artificial Intelligence

摘要

This grant impacted several projects undertaken by investigators. The METEORtheorem proving project focussed on a parallel implementation of the Model Elimination proof procedure, but discovered that the sequential version is also very powerful. The Near-Horn Prolog addresses disjunctive logic programming, which extends Horn clause logic (Prolog) by allowing clauses with multiple positive literals. The lambdaProlog project investigates foundational and implementation related aspects of a Prolog extension that incorporates higher-order logic terms and new search primitives into the Horn clause logic framework. The resulting language has been shown to be useful for prototyping new inference-oriented software. The final project is really several projects in learning; foundational, utilizing connectionism, and learning real-time programs.