{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:20Z","timestamp":1759017920991,"version":"3.44.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032060846","type":"print"},{"value":"9783032060853","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"Abstract<\/jats:title>\n Levesque and Lakemeyer proposed a logic called \n \n $$\\mathcal L$$<\/jats:tex-math>\n \n L<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> as a first-order logic for knowledge representation and reasoning in knowledge-based systems. A characteristic feature of this logic is that it uses a countably infinite set of what are called standard names, which are syntactically treated like constants, but which are also isomorphic to a fixed universe of discourse. Quantifiers in \n \n $$\\mathcal L$$<\/jats:tex-math>\n \n L<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> are then given a substitutional interpretation. This non-standard semantics not only simplifies the proofs for certain meta-theoretic properties, but is also exploited in dedicated reasoning procedures for modal extensions of \n \n $$\\mathcal L$$<\/jats:tex-math>\n \n L<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> that include notions of belief, actions, time, and more. However, the only sound and complete proof system provided for \n \n $$\\mathcal L$$<\/jats:tex-math>\n \n L<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> so far is a Hilbert-style axiom system, as well as an iterative reasoning mechanism based on resolution and clause subsumption. In this paper, we present a tableau system for \n \n $$\\mathcal L$$<\/jats:tex-math>\n \n L<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, and show its soundness and completeness. Completeness is proved first by reduction to the existing axiom system, and involves the cut rule, and then via Hintikka sets, which does not require the cut rule.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_2","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:06Z","timestamp":1758969906000},"page":"22-38","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Tableau System for\u00a0First-Order Logic with\u00a0Standard Names"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0395-1907","authenticated-orcid":false,"given":"Jens","family":"Cla\u00dfen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4582-1702","authenticated-orcid":false,"given":"Torben","family":"Bra\u00fcner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"issue":"2","key":"2_CR1","doi-asserted-by":"publisher","first-page":"226","DOI":"10.2307\/2271099","volume":"34","author":"J Barwise","year":"1969","unstructured":"Barwise, J.: Infinitary logic and admissible sets. J. Symb. Logic 34(2), 226\u2013252 (1969). https:\/\/doi.org\/10.2307\/2271099","journal-title":"J. Symb. Logic"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Beckert, B.: Equality and other theories. In: D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 197\u2013254. Springer, Dordrecht (1999). https:\/\/doi.org\/10.1007\/978-94-017-1754-0_4","DOI":"10.1007\/978-94-017-1754-0_4"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Beckert, B., Posegga, J.: LeanTAP: lean tableau-based deduction. J. Autom. Reason. 15(3), 339\u2013358 (1995)","DOI":"10.1007\/BF00881804"},{"key":"2_CR4","unstructured":"Bell, J.L.: Infinitary Logic. In: Zalta, E.N., Nodelman, U. (eds.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Fall 2023 edn. (2023)"},{"key":"2_CR5","unstructured":"Cla\u00dfen, J., Eyerich, P., Lakemeyer, G., Nebel, B.: Towards an integration of Golog and planning. In: Veloso, M.M. (ed.) Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 1846\u20131851. AAAI Press (2007)"},{"key":"2_CR6","unstructured":"Cla\u00dfen, J., Lakemeyer, G.: A logic for non-terminating Golog programs. In: Brewka, G., Lang, J. (eds.) Proceedings of the Eleventh International Conference on the Principles of Knowledge Representation and Reasoning (KR 2008), pp. 589\u2013599. AAAI Press (2008)"},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Cla\u00dfen, J., Neuss, M.: Knowledge-based programs with defaults in a modal situation calculus. In: Kaminka, G.A., et al. (eds.) Proceedings of the Twenty-Second European Conference on Artificial Intelligence (ECAI 2016), pp. 1309\u20131317. IOS Press (2016). https:\/\/doi.org\/10.3233\/978-1-61499-672-9-1309","DOI":"10.3233\/978-1-61499-672-9-1309"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"D\u2019Agostino, M., Mondadori, M.: The taming of the cut. Classical refutations with analytical cut. J. Logic Comput. 4, 285\u2013319 (1994)","DOI":"10.1093\/logcom\/4.3.285"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Fitting, M.: Modal proof theory. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, pp. 85\u2013138. Elsevier (2007)","DOI":"10.1016\/S1570-2464(07)80005-X"},{"key":"2_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M Fitting","year":"1996","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Cham (1996)","edition":"2"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Hofmann, T., Cla\u00dfen, J.: LTLf synthesis on first-order agent programs in nondeterministic environments. In: Walsh, T., Shah, J., Kolter, Z. (eds.) Proceedings of the Thirty-Ninth AAAI Conference on Artificial Intelligence (AAAI 2025), pp. 14976\u201314986. AAAI Press (2025). https:\/\/doi.org\/10.1609\/aaai.v39i14.33642","DOI":"10.1609\/aaai.v39i14.33642"},{"key":"2_CR12","unstructured":"Jeffrey, R.: Formal Logic: Its Scope and Limits. McGraw Hill (1967)"},{"issue":"1","key":"2_CR13","doi-asserted-by":"publisher","first-page":"4","DOI":"10.2178\/bsl\/1080330272","volume":"10","author":"HJ Keisler","year":"2004","unstructured":"Keisler, H.J., Knight, J.F.: Barwise: infinitary logic and admissible sets. Bull. Symb. Logic 10(1), 4\u201336 (2004). https:\/\/doi.org\/10.2178\/bsl\/1080330272","journal-title":"Bull. Symb. Logic"},{"key":"2_CR14","unstructured":"Kreisel, G.: Set theoretic problems suggested by the notion of potential totality. In: Infinitistic Methods (Proc. Sympos. Foundations of Math., Warsaw, 1959), pp. 103\u2013140 (1961)"},{"key":"2_CR15","unstructured":"Kripke, S.A.: Is there a problem about substitutional quantification? In: Evans, G., McDowell, J. (eds.) Truth and Meaning: Essays in Semantics, pp. 324\u2013419. Clarendon Press (1976)"},{"key":"2_CR16","volume-title":"Naming and Necessity: Lectures Given to the Princeton University Philosophy Colloquium","author":"SA Kripke","year":"1980","unstructured":"Kripke, S.A.: Naming and Necessity: Lectures Given to the Princeton University Philosophy Colloquium. Harvard University Press, Cambridge (1980)"},{"issue":"4","key":"2_CR17","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/s10849-009-9117-6","volume":"19","author":"G Lakemeyer","year":"2010","unstructured":"Lakemeyer, G.: The situation calculus: a case for modal logic. J. Logic Lang. Inform. 19(4), 431\u2013450 (2010). https:\/\/doi.org\/10.1007\/s10849-009-9117-6","journal-title":"J. Logic Lang. Inform."},{"key":"2_CR18","unstructured":"Lakemeyer, G., Levesque, H.J.: Only-knowing meets nonmonotonic modal logic. In: Brewka, G., Eiter, T., McIlraith, S.A. (eds.) Proceedings of the Thirteenth International Conference on the Principles of Knowledge Representation and Reasoning (KR 2012). AAAI Press (2012)"},{"key":"2_CR19","doi-asserted-by":"publisher","unstructured":"Lakemeyer, G., Levesque, H.J.: A tractable, expressive, and eventually complete first-order logic of limited belief. In: Kraus, S. (ed.) Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI 2019), pp. 1764\u20131771. ijcai.org (2019). https:\/\/doi.org\/10.24963\/ijcai.2019\/244","DOI":"10.24963\/ijcai.2019\/244"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Letz, R.: First-order tableau methods. In: D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 125\u2013196. Springer, Dordrecht (1999). https:\/\/doi.org\/10.1007\/978-94-017-1754-0_3","DOI":"10.1007\/978-94-017-1754-0_3"},{"key":"2_CR21","unstructured":"Levesque, H.J., Lakemeyer, G.: The Logic of Knowledge Bases, 2nd edn. College Publications (2022)"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Posegga, J., Schmitt, P.H.: Implementing semantic tableaux. In: D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 581\u2013629. Springer, Dordrecht (1999). https:\/\/doi.org\/10.1007\/978-94-017-1754-0_10","DOI":"10.1007\/978-94-017-1754-0_10"},{"issue":"3","key":"2_CR23","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/BF00243790","volume":"3","author":"SV Reeves","year":"1987","unstructured":"Reeves, S.V.: Adding equality to semantic tableaux. J. Autom. Reason. 3(3), 225\u2013246 (1987). https:\/\/doi.org\/10.1007\/BF00243790","journal-title":"J. Autom. Reason."},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Schmidt, R.A., Tishkovsky, D.: Using tableau to decide description logics with full role negation and identity. ACM Trans. Comput. Logic 15(1), 7:1\u20137:31 (2014). https:\/\/doi.org\/10.1145\/2559947","DOI":"10.1145\/2559947"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Schwering, C.: A reasoning system for a first-order logic of limited belief. In: Bacchus, F., Sierra, C. (eds.) Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI 2017), pp. 5246\u20135248. AAAI Press (2017)","DOI":"10.24963\/ijcai.2017\/779"},{"key":"2_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"RM Smullyan","year":"1968","unstructured":"Smullyan, R.M.: First-Order Logic. Springer, New York (1968)"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Tharp, L.H.: Truth, quantification, and abstract objects. No\u00fbs 5(4), 363\u2013372 (1971)","DOI":"10.2307\/2214383"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Wallace, J.: Convention T and substitutional quantification. No\u00fbs 5(2), 199\u2013211 (1971)","DOI":"10.2307\/2214732"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Zarrie\u00df, B., Cla\u00dfen, J.: Decidable verification of Golog programs over non-local effect actions. In: Schuurmans, D., Wellman, M. (eds.) Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (AAAI 2016), pp. 1109\u20131115. AAAI Press (2016)","DOI":"10.25368\/2022.224"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06085-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:09Z","timestamp":1758969909000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/tableaux\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}