Online research in philosophy

A rational agent (artificial or otherwise) residing in a complex changing environment must gather information perceptually, update that information as the world changes, and combine that information with causal information to reason about the changing world. Using the system of defeasible reasoning that is incorporated into the OSCAR architecture for rational agents, a set of reasonschemas is proposed for enabling an agent to perform some of the requisite reasoning. Along the way, solutions are proposed for the Frame Problem, the Qualification Problem, and the Ramification Problem. The principles and reasoning described have all been implemented in OSCAR.

The objective of the OSCAR Project is twofold. On the one hand, it is to construct a general theory of rational cognition. On the other hand, it is to construct an artificial rational agent (an "artilect") implementing that theory. This is a joint project in philosophy and AI.

Most automated theorem provers are clausal-form provers based on variants of resolutionrefutation. In my [1990], I described the theorem prover OSCAR that was based instead on natural deduction. Some limited evidence was given suggesting that OSCAR was suprisingly efficient. The evidence consisted of a handful of problems for which published data was available describing the performance of other theorem provers. This evidence was suggestive, but based upon too meager a comparison to be conclusive. The question remained, “How does natural deduction compare with resolution-refutation?” In the ensuing seven years, OSCAR has evolved in important ways, and other developments have made it possible to collect more accurate comparative data. Specifically, the creation of the TPTP library of problems for theorem provers,1 and the availability of important theorem provers on the world wide web, make objective comparisons easier. These developments recently inspired Geoff Sutcliffe, one of the founders of the TPTP library, to issue a challenge to OSCAR. At CADE-13, a competition was held for clausal-form theorem provers.2 Otter was one of the most successful contestants. In addition, Otter is able to handle problems stated in natural form (as opposed to clausal form), and Otter is readily available for different platforms.3 Sutcliffe selected 212 problems from the TPTP library, and suggested that OSCAR and Otter run these problems on the same hardware. This “Shootout at the ATP corral” took place, with the result that OSCAR was on the average 40 times faster than Otter. In addition, OSCAR was able to find proofs for 16 problems on which Otter failed, and Otter was able to find proofs for 3 problems on which OSCAR failed. Taking into account that Otter was written in C and OSCAR in LISP, the speed difference of the algorithms themselves could be as much as an order of magnitude greater. Apparently, natural deduction has some advantages over resolution-refutation..

He then argues that (1), (2) and (3) constitute an inconsistent triad as follows (1991, p. 15): Suppose (1) that Oscar knows a priori that he is thinking that water is wet. Then by (2), Oscar can simply deduce E, using premisses that are knowable a priori, including the premiss that he is thinking that water is wet. Since Oscar can deduce E from premisses that are knowable a priori, Oscar can know E itself a priori. But this contradicts (3), the assumption that E cannot be known a priori. Hence (1), (2), and (3) are inconsistent. McKinsey’s conclusion is that ‘anti-individualism is inconsistent with privileged access’ (ibid.).

The “grand problem” of AI has always been to build artificial agents with human-like intelligence. That is the stuff of science fiction, but it is also the ultimate aspiration of AI. In retrospect, we can understand what a difficult problem this is, so since its inception AI has focused more on small manageable problems, with the hope that progress there will have useful implications for the grand problem. Now there is a resurgence of interest in tackling the grand problem head-on. Perhaps AI has made enough progress on the little problems that we can fruitfully address the big problem. The objective is to build agents of human-level intelligence capable of operating in environments of real-world complexity. I will refer to these as GIAs — “generally intelligent agents”. OSCAR is a cognitive architecture for GIAs, implemented in LISP.1 OSCAR draws heavily on my work in philosophy concerning both epistemology (Pollock 1974, 1986, 1990, 1995, 1998, 2008b, 2008; Pollock and Cruz 1999; Pollock and Oved, 2005) and rational decision making (2005, 2006, 2006a).

Pollock describes an exciting theory of rationality and its partial implementation in OSCAR, a computer system whose descendants will literally be persons.

The “grand problem” of AI has always been to build artificial agents of human-level intelligence, capable of operating in environments of real-world complexity. OSCAR is a cognitive architecture for such agents, implemented in LISP. OSCAR is based on my extensive work in philosophy concerning both epistemology and rational decision making. This paper provides a detailed overview of OSCAR. The main conclusions are that such agents must be capablew of operating against a background of pervasive ignorance, because the real world is too complex for them to know more than a small fraction of what is true. This is handled by giving the agent the power to reason defeasibily. The OSCAR system of defeasible reasoning is sketched. It is argued that if epistemic cognition must be defeasible, planning must also be done defeasibly, and the best way to do that is to reason defeasibly about plans. A sketch is given about how this might work.

The objective of the OSCAR Project is twofold. On the one hand, it is to construct a general theory of rational cognition. On the other hand, it is to construct an artificial rational agent (an "artilect") implementing that theory. This is a joint project in philosophy and AI.