{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T09:42:04Z","timestamp":1649151724157},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. of Comput. Sci. &amp; Technol."],"published-print":{"date-parts":[[1993,1]]},"DOI":"10.1007\/bf02946583","type":"journal-article","created":{"date-parts":[[2008,9,7]],"date-time":"2008-09-07T12:32:42Z","timestamp":1220790762000},"page":"26-37","source":"Crossref","is-referenced-by-count":1,"title":["An introduction to INCAPS system"],"prefix":"10.1007","volume":"8","author":[{"given":"Renwei","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pei","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenhui","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF02946583_CR1","doi-asserted-by":"crossref","unstructured":"McArthur, R. P., Tense Logic. D. Reidel Publishing Company, 1976.","DOI":"10.1007\/978-94-017-3219-2"},{"key":"BF02946583_CR2","doi-asserted-by":"crossref","unstructured":"Rescher, N. and Urquart, A., Temporal Logic. Springer-Verlag, 1971.","DOI":"10.1007\/978-3-7091-7664-1"},{"key":"BF02946583_CR3","unstructured":"Li, R. W., N system: A natural temporal deduction systemChinese, Science Bulletin, 1989, 34 (5)."},{"issue":"3","key":"BF02946583_CR4","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF02943343","volume":"3","author":"R. W. Li","year":"1988","unstructured":"Li R. W., A natural deduction system of temporal logic.J. Computer Science and Technology, 1988, 3 (3), 173\u2013185.","journal-title":"J. Computer Science and Technology"},{"key":"BF02946583_CR5","unstructured":"Li, R. W., INCAPS: An interactive computer aided proving system.Chinese Journal of Computers, 1989, 12 (12)."},{"key":"BF02946583_CR6","doi-asserted-by":"crossref","unstructured":"Szalas, A., Concerning the semantic consequence relation in first-order temporal logic.Theoretical Computer Science, 1986, 47 (3).","DOI":"10.1016\/0304-3975(86)90157-X"},{"key":"BF02946583_CR7","doi-asserted-by":"crossref","unstructured":"Kroger, F., Temporal Logic of Programs Springer-Verlag, 1987.","DOI":"10.1007\/978-3-642-71549-5"},{"key":"BF02946583_CR8","doi-asserted-by":"crossref","unstructured":"Gordon, M., Milner R.et al., A Metalanguage for Interactive Proof in LCF Conf Record of the Fifth Annual ACM Symp. Principles of Programming Language, 1978.","DOI":"10.1145\/512760.512773"},{"key":"BF02946583_CR9","first-page":"445","volume":"170","author":"D. A. Schmidt","year":"1984","unstructured":"Schmidt, D. A., A programming notation for tactical reasoning. Seventh Conf. Automated Deduction Springer LNCS 170, 1984, 445\u2013459.","journal-title":"Springer LNCS"},{"issue":"4","key":"BF02946583_CR10","first-page":"23","volume":"2","author":"He Pei","year":"1991","unstructured":"He Pei, Proof strategies and validity.Journal of Software (in Chinese), 1991, 2 (4), 23\u201330.","journal-title":"Journal of Software"},{"key":"BF02946583_CR11","unstructured":"Tang, C. S., XYZ: A Program Development Environment Based on Temporal Logic. Programming Languages and System Design (J. Bormann Ed.) 1983."},{"key":"BF02946583_CR12","unstructured":"Tang, C. S., An Introduction to XYZ System. Techn. Rept. IS-CAS-XYZ-88-1, 1988."},{"issue":"3","key":"BF02946583_CR13","first-page":"15","volume":"1","author":"X Miao","year":"1990","unstructured":"Miao X and Tang, C. S., A methodology and an environment for stepwise refinement\u2014according to design decisions.Journal of Software (in Chinese), 1990, 1 (3), 15\u201328.","journal-title":"Journal of Software"},{"key":"BF02946583_CR14","unstructured":"Xie, H. H., A Structured Temporal Logic Language: XYZ\/SE and Its Verification. Techn. Rept. IS-CAS-XYZ-88-3, 1988."},{"key":"BF02946583_CR15","doi-asserted-by":"crossref","unstructured":"Gordon, M. J. C., Milner, R. and Wadsworth, C. P., Edinburgh LCF: A Mechanized Logic of Computation. LNCS 78, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"BF02946583_CR16","unstructured":"Paulson, L. C., Interactive Theorem Proving with Cambridge LCF, A user's Manual. Techn. Rept. No. 80, Computer Laboratory, Univ. of Cambridge, 1985."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02946583.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02946583\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02946583","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T16:17:12Z","timestamp":1558455432000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02946583"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,1]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1993,1]]}},"alternative-id":["BF02946583"],"URL":"https:\/\/doi.org\/10.1007\/bf02946583","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,1]]}}}