{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:50:33Z","timestamp":1759146633583},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2013,9,18]],"date-time":"2013-09-18T00:00:00Z","timestamp":1379462400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10817-013-9292-7","type":"journal-article","created":{"date-parts":[[2013,9,17]],"date-time":"2013-09-17T06:28:57Z","timestamp":1379399337000},"page":"361-378","source":"Crossref","is-referenced-by-count":9,"title":["Using Isabelle\/HOL to Verify First-Order Relativity Theory"],"prefix":"10.1007","volume":"52","author":[{"given":"Mike","family":"Stannett","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Istv\u00e1n","family":"N\u00e9meti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,9,18]]},"reference":[{"key":"9292_CR1","first-page":"1","volume-title":"First-Order Logic Revisited","author":"H Andr\u00e9ka","year":"2004","unstructured":"Andr\u00e9ka, H., Madar\u00e1sz, J.X., N\u00e9meti, I.: Logical analysis of relativity theories. In: Hendricks, H., et al. (eds.) First-Order Logic Revisited, pp. 1\u201330. Logos-Verlag, Berlin (2004)"},{"issue":"2","key":"9292_CR2","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/s11225-008-9125-6","volume":"89","author":"H Andr\u00e9ka","year":"2008","unstructured":"Andr\u00e9ka, H., Madar\u00e1sz, J.X., N\u00e9meti, I., Sz\u00e9kely, G.: Axiomatizing relativistic dynamics without conservation postulates. Stud. Logica 89(2), 163\u2013186 (2008)","journal-title":"Stud. Logica"},{"key":"9292_CR3","unstructured":"Wenzel, M.: The Isabelle\/Isar reference manual. Online: http:\/\/isabelle.in.tum.de\/dist\/Isabelle2012\/doc\/isar-ref.pdf (2012)"},{"key":"9292_CR4","volume-title":"Relativity: The Special and General Theory","author":"A Einstein","year":"1920","unstructured":"Einstein, A.: Relativity: The Special and General Theory. Henry Holt, New York (1920)"},{"issue":"3","key":"9292_CR5","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1007\/s11229-011-9914-8","volume":"186","author":"H Andr\u00e9ka","year":"2012","unstructured":"Andr\u00e9ka, H., Madar\u00e1sz, J.X., N\u00e9meti, I., Sz\u00e9kely, G.: A logic road from special relativity to general relativity. Synthese 186(3), 633\u2013649 (2012)","journal-title":"Synthese"},{"key":"9292_CR6","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1112\/plms\/s2-42.1.230","volume":"42","author":"AM Turing","year":"1937","unstructured":"Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc., Series 2 42, 230\u2013265 (1937, submitted May 1936)","journal-title":"Proc. Lond. Math. Soc., Series 2"},{"key":"9292_CR7","first-page":"173","volume":"5","author":"M Hogarth","year":"1992","unstructured":"Hogarth, M.: Does general relativity allow an observer to view an eternity in a finite time? Found. Phys. Lett. 5, 173\u2013181 (1992)","journal-title":"Phys. Lett."},{"key":"9292_CR8","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1086\/289716","volume":"5","author":"J Earman","year":"1993","unstructured":"Earman, J., Norton, J.: Forever is a day: supertasks in Pitowsky and Malament-Hogarth spacetimes. Philos. Sci. 5, 22\u201342 (1993)","journal-title":"Philos. Sci."},{"key":"9292_CR9","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1023\/A:1014019225365","volume":"41","author":"G Etesi","year":"2002","unstructured":"Etesi, G., N\u00e9meti, I.: Non-turing computations via Malament-Hogarth space-times. Int. J. Theor. Phys. 41, 341\u2013370 (2002). Online: arXiv: gr-qc\/0104023v2","journal-title":"Int. J. Theor. Phys."},{"key":"9292_CR10","doi-asserted-by":"crossref","first-page":"681","DOI":"10.1093\/bjps\/55.4.681","volume":"55","author":"M Hogarth","year":"2004","unstructured":"Hogarth, M.: Deciding arithmetic using SAD computers. Br. J. Philos. Sci. 55, 681\u2013691 (2004)","journal-title":"Br. J. Philos. Sci."},{"key":"9292_CR11","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/s10701-009-9390-x","volume":"40","author":"JB Manchak","year":"2010","unstructured":"Manchak, J.B.: On the possibility of supertasks in general relativity. Found. Phys. 40, 276\u2013288 (2010)","journal-title":"Found. Phys."},{"key":"9292_CR12","doi-asserted-by":"crossref","unstructured":"Andr\u00e9ka, H., N\u00e9meti, I., Sz\u00e9kely, G.: Closed timelike curves in relativistic computation. Online: arXiv: 1105.0047 [gr-qc] (2012)","DOI":"10.1142\/S0129626412400105"},{"key":"9292_CR13","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1016\/j.amc.2005.09.067","volume":"178","author":"M Stannett","year":"2006","unstructured":"Stannett, M.: The case for hypercomputation. Appl. Math. Comput. 178, 8\u201324 (2006)","journal-title":"Appl. Math. Comput."},{"key":"9292_CR14","unstructured":"Sz\u00e9kely, G.: First-order logic investigation of relativity theory with an emphasis on accelerated observers. PhD thesis, E\u00f6tv\u00f6s Lor\u00e1nd University (2009). Online: http:\/\/arxiv.org\/pdf\/1005.0973.pdf"},{"key":"9292_CR15","unstructured":"G\u00f6m\u00f6ri, M., Szab\u00f3, L.E.: On the formal statement of the special principle of relativity. Online: http:\/\/philsci-archive.pitt.edu\/9151\/4\/MG-LESz-math-rel-preprint-v3.pdf (2011)"},{"key":"9292_CR16","unstructured":"Sundar G., N., Bringsjord, S., Taylor, J.: Proof verification and proof discovery for relativity. In: First International Conference on Logic and Relativity: Honoring Istv\u00e1n N\u00e9meti\u2019s 70th birthday, 8\u201312 September 2012, Budapest. R\u00e9nyi Institute, Budapest (2012). Online: http:\/\/www.renyi.hu\/conferences\/nemeti70\/LR12Talks\/govindarejulu-bringsjord.pdf"},{"key":"9292_CR17","first-page":"70","volume-title":"UCNC. Lecture Notes in Computer Science, vol. 7445","author":"E Csuhaj-Varj\u00fa","year":"2012","unstructured":"Csuhaj-Varj\u00fa, E., Gheorghe, M., Stannett, M.: P systems controlled by general topologies. In: Durand-Lose, J., Jonoska, N. (eds.) UCNC. Lecture Notes in Computer Science, vol. 7445, pp. 70\u201381. Springer, Berlin (2012)"},{"key":"9292_CR18","doi-asserted-by":"crossref","unstructured":"N\u00e9meti, P., Sz\u00e9kely, G.: Existence of faster than light signals implies hypercomputation already in special relativity. In: Cooper, S.B., Dawar, A., L\u00f6we, B. (eds.) How the World Computes: Turing Centenary Conference and 8th Conference on Computability in Europe, CiE 2012, 18\u201323 June 2012, Cambridge, UK, Proceedings. Lecture Notes in Computer Science, vol. 7318, pp. 528\u2013538. Springer, Berlin Heidelberg (2012)","DOI":"10.1007\/978-3-642-30870-3_53"},{"key":"9292_CR19","unstructured":"Sz\u00e9kely, G.: The existence of superluminal particles is consistent with the kinematics of Einstein\u2019s special theory of relativity. Online: arXiv: 1202.5790 [physics.gen-ph] (2012)"},{"issue":"5","key":"9292_CR20","doi-asserted-by":"crossref","first-page":"681","DOI":"10.1007\/s10701-005-9041-9","volume":"36","author":"JX Madar\u00e1sz","year":"2006","unstructured":"Madar\u00e1sz, J.X., N\u00e9meti, I., Sz\u00e9kely, G.: Twin Paradox and the logical foundation of relativity theory. Found. Phys. 36(5), 681\u2013714 (2006)","journal-title":"Found. Phys."},{"key":"9292_CR21","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1093\/mind\/LIX.236.433","volume":"59","author":"AM Turing","year":"1950","unstructured":"Turing, A.M.: Computing machinery and intelligence. Mind 59, 433\u2013460 (1950)","journal-title":"Mind"},{"key":"9292_CR22","first-page":"78","volume-title":"Membrane Computing. Lecture Notes in Computer Science, vol. 7762","author":"M Stannett","year":"2013","unstructured":"Stannett, M.: Membrane systems and hypercomputation. In: Csuhaj-Varj\u00fa, E., Gheorghe, M., Rozenberg, G., Salomaa, A., Vaszil, G. (eds) Membrane Computing. Lecture Notes in Computer Science, vol. 7762, pp. 78\u201387. Springer, Berlin Heidelberg (2013)"},{"key":"9292_CR23","doi-asserted-by":"crossref","first-page":"1075","DOI":"10.1088\/0004-637X\/692\/2\/1075","volume":"692","author":"S Gillessen","year":"2009","unstructured":"Gillessen, S., Eisenhauer, F., Trippe, S., Alexander, T., Genzel, R., Martins, F., Ott, T.: Monitoring stellar orbits around the massive black hole in the Galactic center. Astrophys. J. 692, 1075\u20131109 (2009)","journal-title":"Astrophys. J."},{"key":"9292_CR24","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1016\/j.amc.2005.09.075","volume":"178","author":"I N\u00e9meti","year":"2006","unstructured":"N\u00e9meti, I., D\u00e1vid, G.: Relativistic computers and the Turing barrier. Appl. Math. Comput. 178, 118\u2013142 (2006)","journal-title":"Appl. Math. Comput."},{"key":"9292_CR25","first-page":"398","volume-title":"Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, July 2006, Swansea, UK, Proceedings. Lecture Notes in Computer Science, vol. 3988","author":"I N\u00e9meti","year":"2006","unstructured":"N\u00e9meti, I., Andr\u00e9ka, H.: Can general relativistic computers break the Turing barrier? In: Beckmann, A., Berger, U., L\u00f6we, B., Tucker, J.V. (eds.) Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, July 2006, Swansea, UK, Proceedings. Lecture Notes in Computer Science, vol. 3988, pp. 398\u2013412. Springer, Berlin Heidelberg (2006)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9292-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9292-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9292-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,24]],"date-time":"2019-07-24T04:35:11Z","timestamp":1563942911000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9292-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,18]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["9292"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9292-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9,18]]}}}