Automated reasoning in geometry theorem proving with Prolog. (English) Zbl 0642.68161
Summary: This paper describes automated reasoning in a PROLOG Euclidean geometry theorem-prover. It brings into focus general topics in automated reasoning and the ability of Prolog in coping with them.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 51-04 | Software, source code, etc. for problems pertaining to geometry |
Keywords:
logic programming; knowledge representation; heuristics; automated reasoning; geometry theorem-proverSoftware:
Geometry TutorReferences:
| [1] | Anderson, J. R., ?Turning of search of the problem space for geometry proofs? Proc. of the 7th IJCAI (1981). |
| [2] | Anderson, J. R., Boyle, C. F., Yost, G., The Geometry Tutor, Proc. of the 9th IJCAI (1985). |
| [3] | Coelho, H., ?An inquiry on the geometry machine and its extensions with a review of previous work,? Working report No. 1 for INVOTAN (1974). |
| [4] | Coelho, H., Cotta, J. C., and Pereira, L. M., ?How to solve it with Prolog?, LNEC 2nd. edition (1982). |
| [5] | Clocksin, W. and Mellish, C., Programming in Prolog Springer-Verlag (1981). |
| [6] | van Emden, M., Programming with Resolution Logic, Research report CS-75-30, University of Waterloo (1975). |
| [7] | Fearnley-Sander, D. ?Using and computing symmetry in geometry proofs?, in (ed. Ross, P.) Proc. of AISB-84 (1985). |
| [8] | Gelernter, H. and Rochester, N., ?Intelligent behaviour in problem-solving machines?, IBM Journal, October (1958). |
| [9] | Gelernter, H., ?A note on syntactic symmetry and the manipulation of formal systems by machine?, Information and Control No. 2 (1959). · Zbl 0092.13402 |
| [10] | Gelernter, H., ?Realization of a geometry theorem proving machine?, Proc. Int. Conf. on Information Processing (1959). · Zbl 0092.13402 |
| [11] | Gilmore, P. C., ?An examination of the geometry theorem machine?. Artificial Intelligence 1 (1970), 171-187. · Zbl 0205.31602 · doi:10.1016/0004-3702(70)90005-6 |
| [12] | Goldstein, I., Elementary Geometry Theorem Proving, MIT, AI Lab memo no. 280 (April 1973). |
| [13] | Nevins, A., ?Plane geometry theorem proving using forward chaining?, Artificial Intelligence No. 1 (Spring 1975). · Zbl 0301.68086 |
| [14] | Pereira, L. M. and Meltzer, B., ?Implementation of an efficient predicate logic interpreter based on Earley deduction?, Scientific Proposal report for the SRC (April 1975). |
| [15] | Reiter, R., ?The use of models in automatic theorem-proving?, Univ. of British Columbia, Techn. report 72-04 (Sept. 1972). |
| [16] | Roussel, P., ?Prolog ? Manuel de reference et d’utilization?, G.I.A., U.E.R. de Luminy, Univ. d’AixMarseille, 1975. |
| [17] | Warren, D., ?Epilog: an users’ guide to DEC-10 Prolog?, DAI report, Univ. of Edinburgh (August 1975). |
| [18] | Welham, R., ?G,a geometry theorem prover?, (unpublished) (March 1975). |
| [19] | Welham, R., ?Geometry problem solving?, D.A.I. Research Report No. 14 (January 1976). |
| [20] | Wen-Tsun, W., ?Some recent advances in mechanical theorem-proving of geometries?, in Contemporary Mathematics: Automated Theorem Proving after 25 Years, American Mathematical Society, Volume 29, 1984. |
| [21] | Wen-Tsun, W., ?On the decision problem and the mechanization of theorem-proving in elementary geometry?, in Contemporany Mathematics: Automated Theorem Proving After 25 Years, American Mathematical Society, Vol. 29, 1984. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
