{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T04:48:37Z","timestamp":1769748517323,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540614746","type":"print"},{"value":"9783540685999","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61474-5_83","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:41:33Z","timestamp":1330274493000},"page":"360-371","source":"Crossref","is-referenced-by-count":24,"title":["Automatic translation of natural language system specifications into temporal logic"],"prefix":"10.1007","author":[{"given":"Rani","family":"Nelken","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nissim","family":"Francez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"31_CR1","unstructured":"E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the futurebus+ cache coherence protocol. In L. Claesen, editor, Proceedings of the Eleventh International Symposium on Computer Hardware Description Langugages and their Applications, North Holland, 1993."},{"issue":"2","key":"31_CR2","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Expressibility results for linear time and branching time logic. ACM transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM transactions on Programming Languages and Systems"},{"key":"31_CR3","volume-title":"Computational Aspects of Constraint \u2014 Based Linguistic Description, volume I","author":"J. D\u00f6rre","year":"1993","unstructured":"J. D\u00f6rre and M. Dorna. Cuf \u2014 a formalism for linguistic knowledge representation. In J. D\u00f6rre, editor, Computational Aspects of Constraint \u2014 Based Linguistic Description, volume I. ILLC\/Department of Philosophy, University of Amsterdam, Amsterdam, 1993. DYANA 2 deliverable R.1.2.A."},{"key":"31_CR4","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/BF01384048","volume":"4","author":"A. Fantechi","year":"1994","unstructured":"A. Fantechi, S. Gnesi, G. Ristori, M. Carenini, M. Vanocchi, and P. Moreschini. Assisting requirement formalization by means of natural language translation. Formal Methods in System Design, 4:243\u2013263, 1994.","journal-title":"Formal Methods in System Design"},{"key":"31_CR5","unstructured":"N. E. Fuchs and R. Schwitter. Specifying logic programs in controlled natural language. In Proceedings of the Workshop on Computational Logic for Natural Language Processing. A Joint COMPULOGNET\/ELSNET\/EAGLES Workshop, Edinburgh, 1995."},{"key":"31_CR6","first-page":"180","volume-title":"Lecture Notes in Artificial Intelligence 827","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and R.P. Kurshan. How linear can branching-time be? In D. M. Gabbay and H. J. Ohlbach, editors, First International Conference on Temporal Logic (ICTL '94). Lecture Notes in Artificial Intelligence 827, pages 180\u2013194, Bonn, Germany, 1994. Springer-Verlag."},{"key":"31_CR7","unstructured":"E. W. Hinrichs. Temporale anaphora im englischen. Unpublished Statexamen Thesis. University of Tuebingen., 1981."},{"key":"31_CR8","first-page":"277","volume-title":"Formal Methods in the Study of Language","author":"H. Kamp","year":"1981","unstructured":"H. Kamp. A theory of truth and semantic representation. In T. Janssen J. Groenendijk and M. Stokhof, editors, Formal Methods in the Study of Language, pages 277\u2013322. Mathematical Center, Amsterdam, 1981."},{"key":"31_CR9","unstructured":"H. Kamp and U. Reyle. A calculus for first order discourse representation structures. Bericht Nr.16-1991 Arbeitspapier des Sonderforschungsbereich 340, Institut f\u00fcr Maschinelle Sprachverarbeitung, Universit\u00e4t Stuttgart, 1991."},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"H. Kamp and U. Reyle. From Discourse to Logic, volume 42 of Studies in Linguistics and Philosophy. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-94-011-2066-1"},{"key":"31_CR11","unstructured":"E. K\u00f6nig. A study in grammar design. Arbeitspapier 54 des Sonderforschungsbereich 340. Institut f\u00fcr Maschinelle Sprachverarbeitung, Universit\u00e4t Stuttgart, 1994."},{"key":"31_CR12","unstructured":"E. K\u00f6nig. Lexgram \u2014 a practical categorial grammar formalism. In Proceedings of the Workshop on Computational Logic for Natural Language Processing. A Joint COMPULOGNET\/ELSNET\/EAGLES Workshop, Edinburgh, Scotland, 1995."},{"key":"31_CR13","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1080\/00029890.1958.11989160","volume":"65","author":"J. Lambek","year":"1958","unstructured":"J. Lambek. The mathematics of sentence structure. American mathematical monthly, 65:154\u2013170, 1958.","journal-title":"American mathematical monthly"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems. Springer \u2014 Verlag, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"K. L. Mcmillan. Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University. 1992.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"31_CR16","doi-asserted-by":"crossref","unstructured":"R. Nelken and N. Francez. Splitting the reference time:temporal anaphora and quantification. In Proceedings of the EACL '95 \u2014 The seventh meeting of the European Chapter of the Association for Computational Linguistics, Dublin, Ireland, 1995. Also available as Technical Report LCL-94-10 of the Laboratory for Computational Linguistics, The Technion IIT.","DOI":"10.3115\/976973.977010"},{"key":"31_CR17","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/BF00627707","volume":"7","author":"B. Partee","year":"1984","unstructured":"B. Partee. Nominal and temporal anaphora. Linguistics and Philosophy, 7:243\u2013286, 1984.","journal-title":"Linguistics and Philosophy"},{"key":"31_CR18","volume-title":"Head Driven Phrase Structure Grammar","author":"C. Pollard","year":"1994","unstructured":"C. Pollard and I. A. Sag. Head Driven Phrase Structure Grammar. University of Chicago Press, Chicago, 1994."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61474-5_83.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:06:42Z","timestamp":1605629202000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_83"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_83","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}