{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T10:30:40Z","timestamp":1787049040666,"version":"build-2736575974"},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T00:00:00Z","timestamp":1781568000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T00:00:00Z","timestamp":1781568000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"funder":[{"DOI":"10.13039\/100006199","name":"Langley Research Center","doi-asserted-by":"crossref","award":["80LARC23DA003"],"award-info":[{"award-number":["80LARC23DA003"]}],"id":[{"id":"10.13039\/100006199","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2026,9]]},"DOI":"10.1007\/s00236-026-00540-3","type":"journal-article","created":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T15:17:54Z","timestamp":1781623074000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A natural deduction system for the Byzantine Generals Oral Messages algorithm"],"prefix":"10.1007","volume":"63","author":[{"given":"Dennis M.","family":"Volpano","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,16]]},"reference":[{"key":"540_CR1","unstructured":"Bevier, W., Young, W.: Machine-checked proofs of the design and implementation of a fault-tolerant circuit, Hampton, VA (1990). (182099 Technical Report NASA Contractor Report)"},{"key":"540_CR2","doi-asserted-by":"crossref","unstructured":"Driscoll, K., Hall, B., Paulitsch, M., Zumsteg, P., Sivencrona, H.: The real Byzantine Generals. In: Proc. 23rd IEEE Digital Avionics Systems Conference, pp. 6\u2013416411. (2004)","DOI":"10.1109\/DASC.2004.1390734"},{"issue":"2","key":"540_CR3","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"M Fischer","year":"1985","unstructured":"Fischer, M., Lynch, N., Paterson, M.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"issue":"4","key":"540_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0020-0190(82)90033-3","volume":"14","author":"M Fischer","year":"1982","unstructured":"Fischer, M., Lynch, N.: A lower bound for the time to assure interactive consistency. Inf. Process. Lett. 14(4), 183\u2013186 (1982)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"540_CR5","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L Lamport","year":"1982","unstructured":"Lamport, L., Shostak, R., Pease, M.: The Byzantine Generals Problem. ACMTrans. Program. Lang. Syst. 4(3), 382\u2013401 (1982)","journal-title":"ACMTrans. Program. Lang. Syst."},{"issue":"4","key":"540_CR6","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/190650.190656","volume":"26","author":"W Lloyd","year":"1994","unstructured":"Lloyd, W.: Exploring the Byzantine Generals Problem with beginning computer science students. ACM SIGCSE Bull. 26(4), 21\u201324 (1994)","journal-title":"ACM SIGCSE Bull."},{"key":"540_CR7","volume-title":"Distributed Algorithms","author":"N Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufmann Publishers, San Francisco (1996)"},{"key":"540_CR8","doi-asserted-by":"crossref","unstructured":"Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. J.ACM 27(2), 228\u2013234 (1980)","DOI":"10.1145\/322186.322188"},{"key":"540_CR9","unstructured":"Rushby, J.: Formal Verification of an Oral Messages Algorithm for Interactive Consistency, Hampton, VA (1992). (189704 Technical Report NASA Contractor Report)"},{"key":"540_CR10","doi-asserted-by":"crossref","unstructured":"Tikvati, A., Ben-Ari, M., Kolikant, Y.: Virtual Trees for the Byzantine Generals Algorithm. In: Proc. 35th SIGCSE Technical Symposium on Computer Science Education, pp. 392\u2013396. (2004)","DOI":"10.1145\/971300.971435"},{"issue":"4","key":"540_CR11","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1109\/32.588536","volume":"23","author":"W Young","year":"1997","unstructured":"Young, W.: Comparing verification systems: interactive consistency in ACL2. IEEE Trans. Softw. Eng. 23(4), 214\u2013223 (1997)","journal-title":"IEEE Trans. Softw. Eng."}],"updated-by":[{"DOI":"10.1007\/s00236-026-00545-y","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T00:00:00Z","timestamp":1783555200000}}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-026-00540-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-026-00540-3","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-026-00540-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T10:20:35Z","timestamp":1787048435000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-026-00540-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,16]]},"references-count":11,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,9]]}},"alternative-id":["540"],"URL":"https:\/\/doi.org\/10.1007\/s00236-026-00540-3","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,16]]},"assertion":[{"value":"2 September 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 May 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 June 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 August 2026","order":5,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Update","order":6,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The original online version of this article was revised: due to the incorrect reference section was published in the article","order":7,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 July 2026","order":8,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":9,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":10,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s00236-026-00545-y","URL":"https:\/\/doi.org\/10.1007\/s00236-026-00545-y","order":11,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare no competing interests.","order":1,"name":"Ethics","label":"Conflict of interest","group":{"name":"EthicsHeading","label":"Declarations"}}],"article-number":"22"}}