Reasoning with Bounded Cognitive Resources

Sammanfattning: Reasoning is an essential element of intelligence. Automated reasoning in formal and symbolic systems is a major topic in computer science and artificial intelligence (AI). Programs for computer-assisted and automated theorem proving are being constructed and used by mathematicians and logicians. Recently, there has been a surge in research in inductive reasoning systems. Inductive programming is an example of applying induction to symbolic systems. Most of the reasoning systems in AI are narrow and specialized to particular tasks and domains. Research work in artificial general intelligence (AGI) aims at producing models of AI that are fully or partially independent of task types. AGI systems are ideally able to learn new knowledge and rules that were not intended during their construction. Automatic reasoning systems are traditionally developed by using heuristics to limit the computational resources. This thesis aims to produce models of easoning that use bounded cognitive resources. Since reasoning is a cognitive function, and human cognitive resources (such as working memory) are severely restricted, one possible method of reducing the computational complexity of reasoning systems is to introduce cognitive resources in the system and put limits on them similar to human cognitive limits. Another important aim of this thesis is to unite the deductive and inductive reasoning in symbolic systems, by using Occam's razor as a guiding principle for induction. The thesis uses an exploratory approach to search for a unified model of reasoning in arbitrary domains. This thesis is a collection of published scientific papers, each contributing iteratively to the construction of a larger and domain-independent model of reasoning in symbolic domains. The first two papers present proof formalisms for first-order logic and description logic that produce comprehensible proofs. The second part comprises of five papers, each extending a model of inductive reasoning that can learn axioms of any arbitrary symbolic domain from random examples. Some of the models in the thesis were able to outstrip human performance in arithmetic, logic and number series problems. This is an interdisciplinary thesis that contributes to a number of scientific areas, mainly formal logic and AGI. Further research in this area can potentially lead to a universal reasoner that is able to learn and reason in more complex symbolic systems such as higher order logics and computer programming.