Báo cáo khoa học: Machine Methods for Proving Logical Arguments Expressed in Englis

This paper describes a COMIT program that proves the validity of logical arguments expressed in a restricted form of ordinary English. Some special features include its ability to translate an input argument into logical notation in four progressively refined ways, of which the first pertains to propositional logic and the last three to first-order functional logic; and its ability in many cases to select the "correct" logical translation of an argument, i.e., the translation that yields the simplest proof....
Nội dung trích xuất từ tài liệu:
Báo cáo khoa học: "Machine Methods for Proving Logical Arguments Expressed in Englis" [Mechanical Translation and Computational Linguistics, vol.8, nos.3 and 4, June and October 1965] Machine Methods for Proving Logical Arguments Expressed in English* by Jared L. Darlington, Research Laboratory of Electronics, Massachusetts Institute of Technology This paper describes a COMIT program that proves the validity of logical arguments expressed in a restricted form of ordinary English. Some special features include its ability to translate an input argument into logical notation in four progressively refined ways, of which the first pertains to propositional logic and the last three to first-order functional logic; and its ability in many cases to select the correct logical trans- lation of an argument, i.e., the translation that yields the simplest proof. The logical evaluation part of the program uses a proof procedure al- gorithm that is an amalgam of the one-literal clause rule of Davis- Putnam and the matching algorithm of Guard. It is particularly effi- cient in proving theorems whose matrices in conjunctive normal form contain one or more one-literal clauses (atomic wffs), but it will also prove theorems whose matrices contain only polyliteral clauses. The program has been run on the I.B.M. 7094 computers at M.I.T. and utilizes the time-sharing facilities provided by Project MAC and the Computation Center. immediately reject ungrammatical sequences, mis- Introduction spelled words, etc., and allow the user sitting at a con-A considerable amount of work has recently been sole to retype the problem in whole or in part.done in the general area of automatic translation of The logic translation program developed by theordinary language into the terminology of symbolic present author differs from some of the others in plac-logic. We shall not attempt here to give a general de- ing primary emphasis on the evaluation of arguments,scription of this work, since it has already been sum- a traditional concern of the logician since the ad-marized and discussed in some detail by R. F. Simmons vent of the Aristotelian theory of the syllogism. Anin section 7 of his excellent report, “Answering English argument may be defined semantically as a group ofQuestions by Computer: a Survey”1. Suffice it to say propositions organized into premisses and conclusion,that no one has essayed the construction of a general where the propositions that constitute the premisseslogic translation program that would, taking account provide evidence for the truth of the conclusion. Or anof all the amphibolies and polysemies of natural lan- argument may be defined syntactically as a string ofguage, unambiguously parse any English sentence and permissible sentences that are divided into premissestranslate it into the notation of symbolic logic. The and conclusion by a syntactic marker, such as a wordsyntactic and semantic problems involved ar ...