**Mail folder:**Interlingua Mail**Next message:**hewitt@ai.mit.edu: "Some thoughts on K.I.F. requirements "**Previous message:**sowa@watson.ibm.com: "Some thoughts on K.I.F."

Date: Tue, 7 May 91 18:40:48 -0700 From: John McCarthy <jmc@dec-lite.stanford.edu> Message-id: <9105080140.AA03389@DEC-Lite.Stanford.EDU> To: interlingua@isi.edu Subject: Proposal about logical syntax for Interlingua Reply-To: jmc@cs.stanford.edu

Logical or Reasoning Syntax for Interlingua This note argues that Interlingua should have a logical syntax in addition to the semantics of the language. The term ``logical syntax'' specifically includes the syntax of proofs as used by Carnap. The logical syntax of a monotonic system of mathematical logic is the notion of proof in the language, i.e. the rules that determine when a sequence of formulas constitutes a proof of a sentence in the language. If the system is non-monotonic like Interlingua, then what corresponds to a proof is an {\it argument} for a sentence. It seems to me that we have some choices to make about the precise definition of an argument for a sentence, and I will discuss some of the alternatives. The argument rules do not themselves constitute a proof procedure. Rather proof procedures generate structures of applications of the rules. A given set of proof rules can support a wide variety of proof procedures, and there is no reason to try to standardize proof procedures. Here are some considerations concerning the logical syntax. 1. Some programs will use Interlingua as an internal representation language. These programs will infer new Interlingua sentences from old. Some will do it by methods peculiar to themselves, but if there is a standard set of inference rules including the nonmonotonic rules, then Interlingua arguments will also be exchangeable. 2. Having a logical syntax helps keep the definers of the semantics from making decisions that make argument verifiers, proof procedures (interactive and otherwise), and problem solvers impractical. 3. The logical syntax should admit reasonably short formal proofs in those cases where the informal human argument is short. This requires modifying some of the choices made by mathematical logicians who have been mainly concerned with metatheorems about the logical systems rather than proofs within the systems. 4. The best logical syntax I know of whose expressive power is akin to that of Interlingua is that used by Jussi Ketonen's interactive theorem prover EKL. It is higher order logic, and it contains constructs like functions and predicates of variable arity. It is designed so that a user can make proofs in the system rather than just informal metalinguistic proofs about the system. I don't forsee direct use of EKL, but many of its logical syntactic features are what will be required by Interlingua. I think its features would provide a start on what Interlingua needs. 5. Like many logical systems, it is based on natural deduction in which one makes assumptions, draws conclusions >From them, and then discharges the assumptions by writing implications. 6. EKL contains no features for nonmonotonic reasoning, and these would have to be devised. 7. Here is a proposal for how nonmonotonic reasoning should be treated. It is compatible with Lifschitz's proposal for the semantics of nonmonotonic reasoning. \section{PROPOSAL FOR NONMONOTONIC ARGUMENTS} The conclusions of nonmonotonic reasoning depend on the set of facts that are taken into account. In human reasoning, on takes into account a limited subset of what one knows. This is necessary because of our computational limitations, and it will be also necessary when the reasoner is a machine. We have heuristics that suggest that a conclusion reached with some limited set of facts will still hold when more facts---even all our knowledge---are taken into account. Usually these heuristics work, but perhaps the major source of error in human reasoning is leaving out some important fact. Proposals for nonmonotic reasoning systems omit a discussion of what facts are taken into account. It is often implicit that the reasoner takes into account everything he knows, but this is really possible only for toy databases. I propose that the logical syntax of Interlingua allow the argument generator, human or machine, to be explicit about what subset of the current beliefs is being taken into account. Adventurous reasoners will take small subsets into account and risk error. Supercautious reasoners that take too much into account will risk being unable to reach a conclusion in the available time. The extreme of adventurousness using the logic of defaults is to draw a conclusion from a single default, its premise, and only enough of the consistency part to check the absence of direct denials of what is to be concluded. This corresponds to the behavior of many expert systems. It is good if Interlingua should allow such reasoning strategies and also allows more careful reasoning. This is a semantic notion of resource bounded reasoning, and I think it corresponds pretty well to human resource bounded reasoning.