Proposal about logical syntax for Interlingua

John McCarthy <jmc@dec-lite.stanford.edu>
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.