Logic & Formal Reasoning
Harmonic Grammars for Formal Languages
Basic connectionist principles imply that grammars should take the form of systems of parallel soft constraints defining an optimization problem the solutions to which are the well-formed structures in the language. Such Harmonic Grammars have been successfully applied to a number of problems in the theory of natural languages. Here it is shown that formal languages too can be specified by Harmonic Grammars, rather than by conventional serial rewrite rule systems. 1 HARMONIC GRAMMARS In collaboration with Geraldine Legendre, Yoshiro Miyata, and Alan Prince, I have been studying how symbolic computation in human cognition can arise naturally as a higher-level virtual machine realized in appropriately designed lower-level connectionist networks.The basic computational principles of the approach are these: (1) a. \Vhell analyzed at the lower level, mental representations are distributed patternsof connectionist activity; when analyzed at a higher level, these same representations constitute symbolic structures.
The Difficulties of Learning Logic Programs with Cut
Bergadano, F., Gunetti, D., Trinchero, U.
As real logic programmers normally use cut (!), an effective learning procedure for logic programs should be able to deal with it. Because the cut predicate has only a procedural meaning, clauses containing cut cannot be learned using an extensional evaluation method, as is done in most learning systems. On the other hand, searching a space of possible programs (instead of a space of independent clauses) is unfeasible. An alternative solution is to generate first a candidate base program which covers the positive examples, and then make it consistent by inserting cut where appropriate. The problem of learning programs with cut has not been investigated before and this seems to be a natural and reasonable approach. We generalize this scheme and investigate the difficulties that arise. Some of the major shortcomings are actually caused, in general, by the need for intensional evaluation. As a conclusion, the analysis of this paper suggests, on precise and technical grounds, that learning cut is difficult, and current induction techniques should probably be restricted to purely declarative logic languages.
What Is a Knowledge Representation?
Davis, Randall, Shrobe, Howard, Szolovits, Peter
Although knowledge representation is one of the central and, in some ways, most familiar concepts in AI, the most fundamental question about it -- What is it? -- has rarely been answered directly. Numerous papers have lobbied for one or another variety of representation, other papers have argued for various properties a representation should have, and still others have focused on properties that are important to the notion of representation in general. In this article, we go back to basics to address the question directly. We believe that the answer can best be understood in terms of five important and distinctly different roles that a representation plays, each of which places different and, at times, conflicting demands on the properties a representation should have. We argue that keeping in mind all five of these roles provides a usefully broad perspective that sheds light on some longstanding disputes and can invigorate both research and practice in the field.
Symbolic Model Checking
Kluwer. See also: Symbolic Model Checking: An Approach to the State Explosion Problem. Doctoral thesis, Carnegie Mellon University, 1992 (http://www.kenmcmil.com/pubs/thesis.pdf). J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, Symbolic model checking: 1020 States and beyond, Information and Computation, Volume 98, Issue 2, June 1992, Pages 142-170 (http://www.sciencedirect.com/science/article/pii/089054019290017A). Burch, J. R.; Clarke, E.M.; McMillan, K. L.; Dill, D.L., Sequential circuit verification using symbolic model checking, Design Automation Conference, 1990. Proceedings, 27th ACM/IEEE, vol., no., pp.46,51, 24-28 Jun 1990. (https://ieeexplore.ieee.org/document/114827) Burch, J.R.; Clarke, E.M.; Long, D.E.; McMillan, K.L.; Dill, D.L., Symbolic model checking for sequential circuit verification, Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, vol.13, no.4, pp.401,424, Apr 1994 (https://ieeexplore.ieee.org/document/275352). E. M. Clarke, O. Grumberg, K. L. McMillan, and X. Zhao. 1995. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proceedings of the 32nd annual ACM/IEEE Design Automation Conference (DAC '95). ACM, New York, NY, USA, 427-432 (http://dl.acm.org/citation.cfm?id=217565). Burch, Jerry R.; Clarke, Edmund M.; Long, David E.; McMillan, Kenneth L.; and Dill, David L., Symbolic Model Checking for Sequential Circuit Verification. IEEE Transactions On Computer-Aided Design of Integrated Circuits and Systems, Vol. 13, No. 4, pp. 401-424, April 1994 (http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/Sequential%20circuit%20verification%20using%20symbolic%20model%20checking.pdf).
Neural Computing with Small Weights
Siu, Kai-Yeung, Bruck, Jehoshua
An important issue in neural computation is the dynamic range of weights in the neural networks. Many experimental results on learning indicate that the weights in the networks can grow prohibitively large with the size of the inputs. Here we address this issue by studying the tradeoffs between the depth and the size of weights in polynomial-size networks of linear threshold elements (LTEs). We show that there is an efficient way of simulating a network of LTEs with large weights by a network of LTEs with small weights. To prove these results, we use tools from harmonic analysis of Boolean functions.
Constructing Proofs in Symmetric Networks
This paper considers the problem of expressing predicate calculus in connectionist networksthat are based on energy minimization. Given a firstorder-logic knowledgebase and a bound k, a symmetric network is constructed (like a Boltzman machine or a Hopfield network) that searches for a proof for a given query. If a resolution-based proof of length no longer than k exists, then the global minima of the energy function that is associated with the network represent such proofs. The network that is generated is of size cubic in the bound k and linear in the knowledge size. There are no restrictions on the type of logic formulas that can be represented.
Neural Computing with Small Weights
Siu, Kai-Yeung, Bruck, Jehoshua
Kai-Yeung Siu Dept. of Electrical & Computer Engineering University of California, Irvine Irvine, CA 92717 Jehoshua Bruck IBM Research Division Almaden Research Center San Jose, CA 95120-6099 Abstract An important issue in neural computation is the dynamic range of weights in the neural networks. Many experimental results on learning indicate that the weights in the networks can grow prohibitively large with the size of the inputs. We show that there is an efficient way of simulating a network of LTEs with large weights by a network of LTEs with small weights. To prove these results, we use tools from harmonic analysis of Boolean functions. Our technique is quite general, it provides insights to some other problems.