Intelligible Automated Reasoning: Systems with the Resolution, Induction and Symmetry

• Autorzy: Poliscuk J.E.
• Języki publikacji: EN

Abstrakty

EN

In mathematics, the programs for proving theorems could be instruments for testing the existing proofs and can be used to test hypotheses, and the programs which allow man’s influence on the process of proving could be used to prove new theorems. An independent theoretical contribution is made by the discovery of the adequate rules of deduction and the automatic procedures for proving. The paper presents a short version of the fully automated programmed systems, intended for proving of theorems in the first-order predicate calculus. Proofs in the form of refutations are based on the following rules of derivation: the orderly linear resolution with marked literals (OL- resolution), the rules of binary induction (Prule) and the rules of symmetry.

Słowa kluczowe

EN

artificial intelligence; deduction; induction; predicate logic; resolution; theorem proving

• Wydawca: Wydawnictwo Politechniki Łódzkiej
• Czasopismo: Journal of Applied Computer Science
• Rocznik: 2005
• Tom: Vol. 13, nr 2
• Strony: 7--28
• Opis fizyczny: Bibliogr. 36 poz.

Twórcy

autor

Poliscuk J.E.

• Department of Electrical Engineering, University of Montenegro Cetinjski put bb, Podgoria, Serbia and Montenegro,

Bibliografia

• [1] Abadi M. and Manna Z.: Nonclausal deduction in first-order temporal logic, JACM 1990, 37(2), pp. 279-317.
• [2] Ackerman, Farrell, and Webelhuth: A Theory of Predicates, CSLI Publications, Stanford, CA, 1998.
• [3] Allen J., and Luckham D.: An interactive theorem proving program. In: Machine Intelligence 5 (ed.) Meltzer B. and Michie D., American Elsevier, NY, 1970, pp. 321-326.
• [4] Bajaj C, Khandelwal S., and Siddavanahalli V.: Interactive Symbolic Visualization of Semi-automatic Theorem Proving. In: Technical Report TR-03-37, 2003, Department of Computer Sciences, Austin.
• [5] Bundy A.: The Computer Modelling of Mathematical Reasoning, Academic Press, 1983.
• [6] Chang C. and Lee. CR.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.
• [7] Darlington J. and Burstall M.: A system which automatically improves programs. In: Proc. Internat. Joint Conf. on AI, 1973, pp. 479-485.
• [8] Davis M.: Eliminating the Irrelevant from Mechanical Proofs. In: Proceedings Symp. of Applied Math, 1963, vol. 15, 15-30.
• [9] Davis M., Logemann G. and Loveland D.: A Machine Program for Theorem-Proving, CACM 5, 1962, pp. 394-397.
• [10] Davis M. and Putnam H.: A Computing Procedure for Quantification Theory, JACM 7(3), 1960, pp. 201-215.
• [11] Devedzic V.: Inteligentni informacioni sistemi, DIGIT/FON, Beograd, 2000.
• [12] Duffy D.: Principles of Automated Theorem Proving, John Wiley and Sons, 1991.
• [13] Finzi A., Pirri F. and Reiter R. : Open world planning in the situation circulus. In: AAAI/IAAI, 2000, pp. 754-760.
• [14] Gilmore P.C.: A Proof Method for Quantification Theory, IBM Journal of Research and Development 4, 1960, pp. 28-35.
• [15] Gjone G., Über L. and Skolem T.W.: Contributions to the history, philosophy and methodology of mathematics, Wiss. Z. Greifswald, Ernst-Moritz-Arndt-Univ. Math.-Natur. Reihe 33(1-2), 1984, pp. 19-21.
• [16] Green C: Application of theorem proving to problem solving. In: Proceedings Conf. of Artificial Intelligence, 1969, pp. 219-240.
• [17] Hotomski P.: Sistemi vestacke inteligencije, Tehnicki fakultet "M. Pupin", Zrenjanin, 1995.
• [18] Ireland K. and Rosen M.: Herbrand's Theorem, In: A Classical Introduction to Modern Number Theory, New York: Springer-Verlag, 1990, pp. 241-248.
• [19] Manna Z., and Waldinger R.: The Automatic Synthesis of Systems of Recursive Programs, ACM SIGPLAN Notices, 1977, vol.12, no 8, pp. 29-36.
• [20] Moore S. J.: Proving Theorems about LISP Functions, Journal of the Association for Comp. Machinery, 1975, vol. 22, no 1, pp. 129-144.
• [21] Newell A., Shaw J. C, and Simon H. A.: Chess-playing programs and the problem of complexity, IBM J. Res. Develop. 2:3, 1958, pp.20-25.
• [22] Plaisted A.D. and Yahya A.: A relevance restriction strategy for automated deduction, Artificial Intelligence 144, 2003, pp. 59-93.
• [23] Plaisted A.D. and Yunshan Z.: Ordered Semantic Hyper Linking, Journal of Automated Reasoning 25(3), 2000, pp. 167-217.
• [24] Plaisted A.D.: Theorem Proving. In: Wiley Encyclopedia of Electrical and Electronics Engineering, Volume 21, John G. Webster, editor, 1999, pp. 662-682.
• [25] Poliscuk E.J.: Automatic Programming Systems Dedicated for Proving of Theorems, WSEAS Transactions on Computers, IEE, (Accepted), April 2005.
• [26] Poliscuk E.J.: The Machine Learning Method: Analysis of Experimental Results, Journal of Quantitative Linguistics, Taylor & Francis Group, London, New York, Philadelphia, Singapore and Stockhlom, vol. 11, no 3, 2004, pp. 215-233.
• [27] Poliscuk E.J., and Stojanovic D.R.: The Intelligent Agent: An Analysis of the Experimental Results, WSEAS Transactions on Systems, IEE, 2004, Issue 10, vol. 3, pp. 3248-3253.
• [28] Polišcuk E.J.: The Analysis of Experimental Results of Machine Learning Approach, Journal of Information and Organizational Sciences, IEE, 2003, vol. 27, no 1, pp. 29-42.
• [29] Polišcuk E.J.: The Machine Learning Approach: Analysis of Experimental Results, Journal of Applied Computer Science, IEE, 2003, vol 11, no 1, pp. 61-76.
• [30] Polišcuk E.J.: Adaptive Machine Reinforcement Learning, Schedae Informaticae, Jagiellonian University Krakow (since 1364), 2002, vol. 11, pp. 57-74.
• [31] Polišcuk E.J.: The Analysis of Experimental Results of Reinforcement Learning Systems, The Computer Science Journal of Moldova, MATH, 2002, vol. 10, no 2 (29), pp. 143-168.
• [32] Polišcuk E.J.: Ekspertni sistemi, Informaticka literatura, Podgorica, S&MN, 2004.
• [33] Polišcuk E.J.: The Analysis of Experimental Results of Machine Learning Approach, In: Proceedings of the 19th International Symposium on Information and Communication Technologies, Sarajevo, 2003, CD-ROM proceeding.
• [34] Robinson J. A.: Automatic Deduction with Hyper-resolution, International Journal of Computer Mathematics 1, 1965, pp. 227-234.
• [35] Robinson A., and Voronkov A. (eds.): Handbook of Automated Reasoning Volume I & II, Elsevier and MIT Press, 2001.
• [36] Wos L., Overbeek R., Lusk E. and Boyle J.: Automated Reasoning – Introduction and Applications. Second Edition, McGraw-Hill, 1992.