{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:54:33Z","timestamp":1750308873820,"version":"3.41.0"},"reference-count":2,"publisher":"Association for Computing Machinery (ACM)","issue":"108","license":[{"start":{"date-parts":[[1989,4,1]],"date-time":"1989-04-01T00:00:00Z","timestamp":607392000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGART Bull."],"published-print":{"date-parts":[[1989,4]]},"abstract":"<jats:p>\n            In previous work, the authors (Hausen-Tropper and Finley, 1988) have developed an extension of classical frame systems using generalized interframe relationships and concepts borrowed from modal logic. Such extended frame systems, termed\n            <jats:italic>modal frame systems<\/jats:italic>\n            by the authors, for which a non-deterministic query paradigm was presented, were intended to provide a flexible knowledge representation mechanism that would handle effectively some of the problems arising from exceptions, conflictual information, and defaults in the encoded knowledge. In the present work, an example of a knowledge base using the full richness of the extended frame representation system is presented. The example chosen is taken from an axiomatic development of the existence of real numbers with the intention of representing theorems and their proofs in the extended frames. The intent is to bring out the \"deep structure\" of the proofs, which might help us to better understand the proof discovery process. Thus, a simple syntactic encoding is not sufficient, rather the choice of a deep representation is sought. With such a representation in hand, the acquisition process should be fairly straight forward. A knowledge base built up in this way will then contain a corpus of knowledge about the given field of mathematics and could be interrogated in order to display the theorems of the system, their proofs, and the interrelationships between the proofs, theorems, axioms, and definitions of the system.\n          <\/jats:p>","DOI":"10.1145\/63266.63308","type":"journal-article","created":{"date-parts":[[2007,1,17]],"date-time":"2007-01-17T18:32:02Z","timestamp":1169058722000},"page":"178-179","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A system for the representation of theorems and proofs"],"prefix":"10.1145","author":[{"suffix":"Jr.","given":"M. R.","family":"Finley","sequence":"first","affiliation":[{"name":"Univ. of Quebec at Montreal, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E. B.","family":"Hausen-Tropper","sequence":"additional","affiliation":[{"name":"Univ. of Quebec at Montreal, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[1989,4]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"103","article-title":"Toward a formalization of frame based knowledge representation systems","volume":"1","author":"Finley M. R.","year":"1988","unstructured":"Finley , M. R. , and E. B. Hausen-Tropper ( 1988 ). \" Toward a formalization of frame based knowledge representation systems ,\" Proceedings of Intelligent Tutoring Systems, ITS-88, Montreal , June 1-3 , pp. 103 - 108 Finley, M. R., and E. B. Hausen-Tropper (1988). \"Toward a formalization of frame based knowledge representation systems,\" Proceedings of Intelligent Tutoring Systems, ITS-88, Montreal, June 1-3, pp. 103-108","journal-title":"Proceedings of Intelligent Tutoring Systems, ITS-88, Montreal"},{"key":"e_1_2_1_2_1","volume-title":"Akademische Verlagsgesellschaft","author":"Landau E.","year":"1948","unstructured":"Landau , E. ( 1948 ). Grundlagen des Analysis (Foundations of Analysis) , Akademische Verlagsgesellschaft , Leipzig, 1930, Chelsea Publishing Company Reprint , New York. Landau, E. (1948). Grundlagen des Analysis (Foundations of Analysis), Akademische Verlagsgesellschaft, Leipzig, 1930, Chelsea Publishing Company Reprint, New York."}],"container-title":["ACM SIGART Bulletin"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/63266.63308","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/pdf\/10.1145\/63266.63308","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:15:16Z","timestamp":1750281316000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/63266.63308"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,4]]},"references-count":2,"journal-issue":{"issue":"108","published-print":{"date-parts":[[1989,4]]}},"alternative-id":["10.1145\/63266.63308"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/63266.63308","relation":{},"ISSN":["0163-5719"],"issn-type":[{"type":"print","value":"0163-5719"}],"subject":[],"published":{"date-parts":[[1989,4]]},"assertion":[{"value":"1989-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}