In this paper we describe a first-order logic inference strategy based on information extracted from both, conjunctive and disjunctive, normal forms. We claim that the search problem for a proof can benefit from this further information, extending the heuristic possibilities of resolution and connection proof methods.
A representação de fórmulas lógicas utilizando formas canônicas tem um papel importante na área de prova de teoremas por computador. Embora a transformação para a forma normal conjuntiva e sua posterior simplificação seja um assunto bastante estudado, devido à sua aplicação ao método de prova automática por resolução, a transformação dual, para a forma normal disjuntiva, principalmente para o caso da lógica de primeira ordem, não mereceu a mesma atenção. Neste artigo apresentamos alguns alguns resultados mostrando que, diferentemente da forma normal conjuntiva, a forma normal disjuntiva não é única para a lógica de primeira ordem e que o cálculo de sua forma mínima apresenta diversas sutilezas. Nosso interesse pela determinação da forma disjuntiva tem origem em sua aplicação no método para prova automática de teoremas por transformação dual, proposto recentemente.
The use of canonical representation of logical formulas plays an important role in the automatic theorem proving domain. Although the transformation into conjunctive normal form, and its further simplification, has been extensively studied, because of its application in the resolution method for automatic theorem proving, the dual transformation, into disjunctive normal form, has not deserved the same atention, mainly in the first-order case. In this paper, we present some results that show that, unlikely the conjunctive norma form, the disjunctive normal form is not unique for the first-order case, and that the determination of its minimal form presents several suptilities. Our interest in the disjunctive normal form comes from its application in the dual transformation method for automatic theorem proving, that was recently proposed.
This paper presents two somewhat independent results and sketches a mechanism that could tie these results together to form an automated theorem proving method. The first point is a correct and complete inference method for first-order logic based on the transformation between conjunctive and disjunctive canonical normal forms. This method, although apparently very inefficient, presents interesting properties, such as not presenting external inference rules. The second point is a concurrent algorithm for dual transformation. This algorithm is presented in a general framework that can be specialized to model several formal systems. Finally, based on the representation adopted to define the algorithm, a dual transformation theorem proving method is sketched.
This paper presents a generic model for a cognitive agent based on the hypothesis that the cognitive activity has three main characteristics: self-organization, evolutionary nature and history dependence. According to this model, a cognitive agent presents three levels: reactive, instinctive and cognitive. Each level, together with its lower levels, is intended to model a complete agent, each new level just increasing the behavior complexity. The generic model is instantiated into a computational architecture that integrates connectionist, evolutionary computation and symbolic approaches. In this architecture, the reactive level is an evolutionary environment where each organism is able to functionally link perceptive input -- represented by neural net outputs -- and effector control -- represented by the input to fuzzy control systems or Brooks' architectures. The instinctive level is based on an inductive learning process that optimizes the evolutionary process at the reactive level. This optimization is done through the memorization of the genetic characteristics of the reactive level agents that prove to be useful in handling specific situations. Finally, the cognitive level is based on a specially designed inference method, whose characteristics -- concurrence, globality and symmetry -- allow for a suitable integration between symbolic and subsymbolic modules of the architecture.
This paper presents an algorithm to determine the geometrical representation for the clauses and dual clauses associated with a set of first-order logic theories, given the clause and dual clause geometrical representations of each theory individually.
This paper presents a hierarchical heterogeneous multi-agent society based on a hypercube parallel architecture able to manage, in a distributed way, a first-order logic knowledge base and to draw inferences from it. The knowledge base is structured into theories, composed by sets of formulas. The adopted internal representation of these theories consists of both canonical forms of the formulas that define them. The inference method underlying the deductive capabilities of the architecture is based on the fact that the two canonical forms of a set of formulas can used as a generalized inference rule, giving rise to a complete logical inference method. A prototype of the proposed knowledge representation system, where concurrence is sequentially simulated, has been implemented in Common Lisp/CLOS.
One of the main goals of Distributed Artificial Intelligence is to devise methods to join a community of Computational Agents into a Multi-Agent System, where these agents can cooperate to reach common goals. Cooperation in a Cognitive Agent community is usually supported by an Agent Communication Language (ACL) which allows the agents to exchange knowledge and information through a computer network. In this paper, we propose Parla, a high level agent communication language to cognitive multi-agent systems. This language is based on a standard message format, that contains the necessary information for the message integrity, network security and groupware services to be implemented. These services can either be performed by the lower layers of the system or be included in the high level agent communication support. This message format has a specific slot to store the cooperation language expressions. These expressions consist of a primitive name and an argument, which should be a valid expression of a knowledge representation formalism supported by the cognitive agent. The following aspects of the Parla language are presented: language layers, agent communication support requirements, message format, primitive set and primitive semantics. To demonstrate the language use, a cooperation example among four agents is presented. In this example, each agent has its own specific domain of knowledge but, because of global interdependences, cooperation is necessary. This example refers to the recomposition of part of the South Brazil's electrical network.