The Workshop on Logic-Based Artificial Intelligence (LBAI), sponsored by the National Science Foundation and the American Association for Artificial Intelligence, was held in Washington, D.C., on 13 to 15 June 1999. The workshop was organized by Jack Minker and John McCarthy. The Program Committee members were Krzysztof Apt, John Horty, Sarit Kraus, Vladimir Lifschitz, John McCarthy, Jack Minker, Don Perlis, and Ray Reiter. The purpose of the workshop was to bring together researchers who use logic as a fundamental tool in AI to permit them to review accomplishments, assess future directions, and share their research in LBAI. This article is a summary of the workshop.
The areas selected for discussion at the workshop were abductive and inductive reasoning, applications of theorem proving, commonsense reasoning, computational logic, constraints, logic and high-level robotics, logic and language, logic and planning, logic for agents and actions, logic of causation and action, logic, probability and decision theory, nonmonotonic reasoning, theories of belief, and knowledge representation.
Sessions consisted of one to four lectures. Following the lectures in each session, a discussion was held to assess accomplishments and directions of research related to the topic of the session. In addition, 12 different logic-based systems were discussed briefly, and the systems were demonstrated. A brief synopsis of the lectures and the systems demonstrated follows.
Description of Workshop
In "Abductive and Inductive Reasoning," F. Buccafurri, T. Eiter, G. Gottlob, and N. Leone provided a first step toward integrating model-checking methods with AI. They developed an abstract concept of a system repair problem that is solved by applying logic-based abduction. S. H. Muggleton and F. A. Marginean noted that data-refinement operators in inductive logic programming have been viewed as functions from clauses to sets of clauses. Searches carried out by genetic algorithms allow larger changes by combining pairs of search nodes. They introduce and discuss binary refinement operators within the subsumption lattice that are functions from pairs of clauses to sets of clauses.
In "Applications of Theorem Proving," J. Moore discussed the capabilities of the ACL2 system (the successor of the Boyer-Moore NQTHM prover). ACL2 defines the state of the art in microprocessor verification. It has been used to formally model a Motorola CAP digital signal processor and the Rockwell-Collins JEM1 microprocessor (the world's first silicon JAVA virtual machine). The use of ACL2 uncovered at least four hardware design bugs--bugs that had survived hundreds of millions of test cases--in time to fix them before the processor was shipped. A. Levy addressed data-integration systems that require a flexible mechanism to describe contents of sources. He surveyed the main logic-based languages that have been considered for describing data sources in data-integration systems and the specialized inference techniques developed in this context. P. Nayak and B. Williams dealt with a reactive self-configuring system installed in the National Aeronautics and Space Administration Deep Space 1 spacecraft now in flight. This autonomous system performs failure analysis and correction for a variety of tasks during the years of active service of the spacecraft. D. Gunning spoke about knowledge base projects at the Defense Advanced Research Projects Agency, where general reasoning systems are needed both to handle the general question-answering problem and to reason from first principles in unanticipated situations.
In "Commonsense Reasoning," McCarthy noted that logical AI involves representing knowledge of an agent's world, its goals, and the current situation by sentences in logic. He characterized a large number of concepts that have arisen in research in logical AI. E. Sandewall addressed what the appropriate research methodology is when logic is used in our field. …