Reasoning about reasoning in a meta-level architecture

In this paper we discuss reasoning about reasoning in a multiple agent scenario. We consider agents that are perfect reasoners, loyal, and that can take advantage of both the knowledge and ignorance of other agents. The knowledge representation formalism we use is (full) first order predicate calculus, where different agents are represented by different theories, and reasoning about reasoning is realized via a meta-level representation of knowledge and reasoning. The framework we provide is pretty general: we illustrate it by showing a machine checked solution to the three wisemen puzzle. The agents' knowledge is organized into units: the agent's own knowledge about the world and its knowledge about other agents are units containing object-level knowledge; a unit containing meta-level knowledge embodies the reasoning about reasoning and realizes the link among units. In the paper we illustrate the meta-level architecture we propose for problem solving in a multi-agent scenario; we discuss our approach in relation to the modal one and we compare it with other meta-level architectures based on logic. Finally, we look at a class of applications that can be effectively modeled by exploiting the meta-level approach to reasoning about knowledge and reasoning.     

The problem of choosing the representation,inference rule,and strategy

This article is the nineteenth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find guidelines for simultaneously choosing the most effective representation, inference rule, and strategy. Since the three areas are tightly coupled, formulation of such guidelines requires understanding the precise nature of this coupling. For evaluating a proposed solution to this research problem, we suggest possible test problems from group theory, Gödel's finite axiomatization of set theory, and program verification.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

Application of parallelized analogical planning to engineering design

Analogical planning provides a means of solving engineering problems where other machine learning methods fail. Unlike many machine learning paradigms, analogy does not require numerous previous examples or a rich domain theory. Instead, analogical planners adapt knowledge of solved problems in similar domains to the current problem. Unfortunately, the analogical planning task is an expensive one. While the process of forming correspondences between a known problem and a new problem is complex, the problem of selecting a base case for the analogy is virtually intractable.This paper addresses the issue of efficiently forming analogical plans. The Anagram planning system is described, which takes advantage of the massively parallel architecture of the Connection Machine to perform base selection and map formation. Anagram provides a tractable solution to analogical planning, with a complexity that is sublinear in the size of the plans.This paper describes the Anagram system and its parallel algorithms. The paper also presents theoretical analyses and empirical results of testing the system on a large database of plans from the domain of automatic programming.     

Philosophical aspects of program verification

A debate over the theoretical capabilities of formal methods in computer science has raged for more than two years now. The function of this paper is to summarize the key elements of this debate and to respond to important criticisms others have advanced by placing these issues within a broader context of philosophical considerations about the nature of hardware and of software and about the kinds of knowledge that we have the capacity to acquire concerning their performance.     

人工智能的应用及困惑

知识获取、知识表示和知识利用成为人工智能的中心问题.但在当前的智能系统中,他们都极不完善.本文通过对人工智能的四大应用领域:专家系统、智能教学系统、自然语言理解及自动程序设计进行分析,说明了在人工智能的应用领域中困难重重.     

建设工程施工合同争议案例知识管理研究

以建设工程施工合同争议案例分解为基础,提出了建设工程施工合同争议案例知识管理模型架构,分析了架构组成.本文将知识元理论和矩阵模型引入到合同争议中,并运用相似度实现案例检索.依据提出的架构及关键技术,承包商企业可实现施工合同争议案例的知识管理,从而提高知识资源的利用率,降低工程成本.     

The problem of self-analytically choosing the set of support

This article is the seventh of a series of articles discussing various open research problems in automated reasoning. Here we focus on self-analysis and the set of support strategy. The problem proposed for research asks for one to find a means for an automated reasoning program to self-analytically determine which clauses to be in the set of support at various points during the program's attempt to complete a given assignment. For evaluating a proposed solution to this research problem, we include suggestions concerning possible test problems.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.     

Human-oriented and machine-oriented reasoning: Remarks on some problems in the history of Automated Theorem Proving

Examples in the history of Automated Theorem Proving are given, in order to show that even a seemingly mechanical activity, such as deductive inference drawing, involves special cultural features and tacit knowledge. Mechanisation of reasoning is thus regarded as a complex undertaking in cultural pruning of human-oriented reasoning. Sociological counterparts of this passage from human- to machine-oriented reasoning are discussed, by focusing on problems of man-machine interaction in the area of computer-assisted proof processing.     

Resource-bounded Relational Reasoning: Induction and Deduction Through Stochastic Matching

One of the obstacles to widely using first-order logic languages is the fact that relational inference is intractable in the worst case. This paper presents an any-time relational inference algorithm: it proceeds by stochastically sampling the inference search space, after this space has been judiciously restricted using strongly-typed logic-like declarations.We present a relational learner producing programs geared to stochastic inference, named STILL, to enforce the potentialities of this framework. STILL handles examples described as definite or constrained clauses, and uses sampling-based heuristics again to achieve any-time learning.Controlling both the construction and the exploitation of logic programs yields robust relational reasoning, where deductive biases are compensated for by inductive biases, and vice versa.