Đang chuẩn bị nút TẢI XUỐNG, xin hãy chờ
Tải xuống
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 | 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 translation of an argument i.e. the translation that yields the simplest proof. The logical evaluation part of the program uses a proof procedure algorithm that is an amalgam of the one-literal clause rule of Davis-Putnam and the matching algorithm of Guard. It is particularly efficient 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. Introduction A considerable amount of work has recently been done in the general area of automatic translation of ordinary language into the terminology of symbolic logic. We shall not attempt here to give a general description of this work since it has already been summarized and discussed in some detail by R. F. Simmons in section 7 of his excellent report Answering English Questions by Computer a Survey 1. Suffice it to say that no one has essayed the construction of a general logic translation program that would taking account of all the amphibolies and polysemies of natural language unambiguously parse any English sentence and translate it into the notation of .
