{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,23]],"date-time":"2024-06-23T00:10:30Z","timestamp":1719101430951},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T00:00:00Z","timestamp":1712102400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T00:00:00Z","timestamp":1712102400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"TU Wien"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Choice logics constitute a family of propositional logics and are used for the representation of preferences, with especially <jats:italic>qualitative choice logic<\/jats:italic> (QCL) being an established formalism with numerous applications in artificial intelligence. While computational properties and applications of choice logics have been studied in the literature, only few results are known about the proof-theoretic aspects of their use. We propose a sound and complete sequent calculus for preferred model entailment in QCL, where a formula\u00a0<jats:italic>F<\/jats:italic> is entailed by a QCL-theory\u00a0<jats:italic>T<\/jats:italic> if\u00a0<jats:italic>F<\/jats:italic> is true in all preferred models of\u00a0<jats:italic>T<\/jats:italic>. The calculus is based on labeled sequent and refutation calculi, and can be easily adapted for different purposes. For instance, using the calculus as a cornerstone, calculi for other choice logics such as <jats:italic>conjunctive choice logic<\/jats:italic> (CCL) and <jats:italic>lexicographic choice logic<\/jats:italic> (LCL) can be obtained in a straightforward way.<\/jats:p>","DOI":"10.1007\/s10817-024-09695-5","type":"journal-article","created":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T15:02:05Z","timestamp":1712156525000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Sequent Calculi for Choice Logics"],"prefix":"10.1007","volume":"68","author":[{"given":"Michael","family":"Bernreiter","sequence":"first","affiliation":[]},{"given":"Anela","family":"Lolic","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Maly","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Woltran","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,3]]},"reference":[{"key":"9695_CR1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2022.103755","volume":"311","author":"M Bernreiter","year":"2022","unstructured":"Bernreiter, M., Maly, J., Woltran, S.: Choice logics and their computational properties. Artif. Intell. 311, 103755 (2022)","journal-title":"Artif. Intell."},{"issue":"1\u20132","key":"9695_CR2","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.artint.2004.04.006","volume":"157","author":"G Brewka","year":"2004","unstructured":"Brewka, G., Benferhat, S., Berre, D.L.: Qualitative choice logic. Artif. Intell. 157(1\u20132), 203\u2013237 (2004)","journal-title":"Artif. Intell."},{"issue":"2","key":"9695_CR3","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1111\/j.0824-7935.2004.00241.x","volume":"20","author":"G Brewka","year":"2004","unstructured":"Brewka, G., Niemel\u00e4, I., Syrj\u00e4nen, T.: Logic programs with ordered disjunction. Comput. Intell. 20(2), 335\u2013357 (2004)","journal-title":"Comput. Intell."},{"issue":"1\u20132","key":"9695_CR4","doi-asserted-by":"publisher","first-page":"7","DOI":"10.3166\/jancl.20.7-37","volume":"20","author":"S Benferhat","year":"2010","unstructured":"Benferhat, S., Sedki, K.: An alert correlation approach based on security operator\u2019s knowledge and preferences. J. Appl. Non Class. Logics 20(1\u20132), 7\u201337 (2010)","journal-title":"J. Appl. Non Class. Logics"},{"key":"9695_CR5","doi-asserted-by":"crossref","unstructured":"Li\u00e9tard, L., Hadjali, A., Rocacher, D.: Towards a gradual QCL model for database querying. In: IPMU (3). Communications in Computer and Information Science, vol. 444, pp. 130\u2013139 (2014). Springer","DOI":"10.1007\/978-3-319-08852-5_14"},{"key":"9695_CR6","doi-asserted-by":"crossref","unstructured":"Sedki, K., Lamy, J., Tsopra, R.: Learning preferences in prioritized qualitative choice logic. In: ICTAI, pp. 368\u2013375 (2020). IEEE","DOI":"10.1109\/ICTAI50040.2020.00065"},{"key":"9695_CR7","doi-asserted-by":"crossref","unstructured":"Sedki, K., Lamy, J., Tsopra, R.: Qualitative choice logic for modeling experts recommendations of antibiotics. In: FLAIRS (2022)","DOI":"10.32473\/flairs.v35i.130677"},{"issue":"1\u20132","key":"9695_CR8","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0004-3702(80)90011-9","volume":"13","author":"J McCarthy","year":"1980","unstructured":"McCarthy, J.: Circumscription - A form of non-monotonic reasoning. Artif. Intell. 13(1\u20132), 27\u201339 (1980)","journal-title":"Artif. Intell."},{"issue":"2","key":"9695_CR9","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1145\/505372.505374","volume":"3","author":"PA Bonatti","year":"2002","unstructured":"Bonatti, P.A., Olivetti, N.: Sequent calculi for propositional nonmonotonic logics. ACM Trans. Comput. Log. 3(2), 226\u2013278 (2002)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1\u20132","key":"9695_CR10","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/0004-3702(80)90014-4","volume":"13","author":"R Reiter","year":"1980","unstructured":"Reiter, R.: A logic for default reasoning. Artif. Intell. 13(1\u20132), 81\u2013132 (1980)","journal-title":"Artif. Intell."},{"issue":"1","key":"9695_CR11","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0004-3702(85)90042-6","volume":"25","author":"RC Moore","year":"1985","unstructured":"Moore, R.C.: Semantical considerations on nonmonotonic logic. Artif. Intell. 25(1), 75\u201394 (1985)","journal-title":"Artif. Intell."},{"key":"9695_CR12","volume-title":"Aristotle\u2019s Syllogistic from the Standpoint of Modern Formal Logic","author":"J \u0141ukasiewicz","year":"1951","unstructured":"\u0141ukasiewicz, J.: Aristotle\u2019s Syllogistic from the Standpoint of Modern Formal Logic. Clarendon Press, Oxford (1951)"},{"key":"9695_CR13","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/BF02121863","volume":"29","author":"J S\u0142upecki","year":"1971","unstructured":"S\u0142upecki, J., Bryll, G., Wybraniec-Skardowska, U.: Theory of rejected propositions. i. Stud. Log. 29, 75\u2013123 (1971)","journal-title":"Stud. Log."},{"key":"9695_CR14","doi-asserted-by":"crossref","unstructured":"Tiomkin, M.L.: Proving unprovability. In: LICS, pp. 22\u201326 (1988). IEEE Computer Society","DOI":"10.1109\/LICS.1988.5097"},{"key":"9695_CR15","unstructured":"Bonatti, P.A.: A gentzen system for non-theorems. In: Technisce Universit\u00e4t Wien, Institut f\u00fcr Informationssysteme, Technical Report CD-TR vol. 93, p. 52 (1993)"},{"key":"9695_CR16","doi-asserted-by":"crossref","unstructured":"Geibinger, T., Tompits, H.: Sequent-type calculi for systems of nonmonotonic paraconsistent logics. In: ICLP Technical Communications. EPTCS, vol. 325, pp. 178\u2013191 (2020)","DOI":"10.4204\/EPTCS.325.23"},{"key":"9695_CR17","first-page":"1","volume-title":"Logic: from Foundations to Applications","author":"A Avron","year":"1996","unstructured":"Avron, A.: The method of hypersequents in the proof theory of propositional nonclassical logics. In: Hodges, W., Hyland, M., Steinhorn, C., Truss, J. (eds.) Logic: from Foundations to Applications, pp. 1\u201332. Oxford Science Publications, Oxford (1996)"},{"key":"9695_CR18","first-page":"193","volume":"4","author":"G Governatori","year":"2006","unstructured":"Governatori, G., Rotolo, A.: Logic of violations: a Gentzen system for reasoning with contrary-to-duty obligations. Aust. J. Logic 4, 193\u2013215 (2006)","journal-title":"Aust. J. Logic"},{"issue":"2","key":"9695_CR19","doi-asserted-by":"publisher","first-page":"473","DOI":"10.2307\/2274395","volume":"52","author":"WA Carnielli","year":"1987","unstructured":"Carnielli, W.A.: Systematization of finite many-valued logics through the method of tableaux. J. Symb. Log. 52(2), 473\u2013493 (1987)","journal-title":"J. Symb. Log."},{"issue":"4","key":"9695_CR20","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10817-013-9273-x","volume":"51","author":"M Baaz","year":"2013","unstructured":"Baaz, M., Lahav, O., Zamansky, A.: Finite-valued semantics for canonical labelled calculi. J. Autom. Reason. 51(4), 401\u2013430 (2013)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9695_CR21","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s11787-021-00274-5","volume":"15","author":"M Kaminski","year":"2021","unstructured":"Kaminski, M., Francez, N.: Calculi for many-valued logics. Log. Univ. 15(2), 193\u2013226 (2021)","journal-title":"Log. Univ."},{"key":"9695_CR22","unstructured":"Boudjelida, A., Benferhat, S.: Conjunctive choice logic. In: ISAIM (2016)"},{"key":"9695_CR23","doi-asserted-by":"crossref","unstructured":"Bernreiter, M., Lolic, A., Maly, J., Woltran, S.: Sequent calculi for choice logics. In: IJCAR, pp. 331\u2013349 (2022). Springer","DOI":"10.1007\/978-3-031-10769-6_20"},{"key":"9695_CR24","unstructured":"Bernreiter, M.: A general framework for choice logics. Master\u2019s thesis, TU Wien (2020)"},{"issue":"1\u20132","key":"9695_CR25","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/0004-3702(90)90101-5","volume":"44","author":"S Kraus","year":"1990","unstructured":"Kraus, S., Lehmann, D., Magidor, M.: Nonmonotonic reasoning, preferential models and cumulative logics. Artif. Intell. 44(1\u20132), 167\u2013207 (1990)","journal-title":"Artif. Intell."},{"issue":"1","key":"9695_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(92)90041-U","volume":"55","author":"D Lehmann","year":"1992","unstructured":"Lehmann, D., Magidor, M.: What does a conditional knowledge base entail? Artif. Intell. 55(1), 1\u201360 (1992)","journal-title":"Artif. Intell."},{"key":"9695_CR27","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"AS Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (2000)"},{"issue":"15","key":"9695_CR28","doi-asserted-by":"publisher","first-page":"1889","DOI":"10.1016\/j.fss.2008.02.014","volume":"159","author":"S Benferhat","year":"2008","unstructured":"Benferhat, S., Sedki, K.: Two alternatives for handling preferences in qualitative choice logic. Fuzzy Sets Syst. 159(15), 1889\u20131912 (2008)","journal-title":"Fuzzy Sets Syst."},{"key":"9695_CR29","unstructured":"Maly, J., Woltran, S.: A new logic for jointly representing hard and soft constraints. In: PRUV@IJCAR. CEUR Workshop Proceedings, vol. 2157 (2018). CEUR-WS.org"},{"key":"9695_CR30","doi-asserted-by":"crossref","unstructured":"Freiman, R., Bernreiter, M.: Truth and preferences - A game approach for qualitative choice logic. In: JELIA. Lecture Notes in Computer Science, vol. 14281, pp. 547\u2013560 (2023). Springer","DOI":"10.1007\/978-3-031-43619-2_37"},{"key":"9695_CR31","doi-asserted-by":"crossref","unstructured":"Freiman, R., Bernreiter, M.: Validity in choice logics - A game-theoretic investigation. In: WoLLIC. Lecture Notes in Computer Science, vol. 13923, pp. 211\u2013226 (2023). Springer","DOI":"10.1007\/978-3-031-39784-4_13"},{"key":"9695_CR32","doi-asserted-by":"crossref","unstructured":"Charalambidis, A., Papadimitriou, G., Rondogiannis, P., Troumpoukis, A.: A Many-valued logic for lexicographic preference representation. In: KR, pp. 646\u2013650 (2021)","DOI":"10.24963\/kr.2021\/62"},{"issue":"5","key":"9695_CR33","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1017\/S1471068421000235","volume":"21","author":"A Charalambidis","year":"2021","unstructured":"Charalambidis, A., Rondogiannis, P., Troumpoukis, A.: A logical characterization of the preferred models of logic programs with ordered disjunction. Theory Pract. Log. Program. 21(5), 629\u2013645 (2021)","journal-title":"Theory Pract. Log. Program."},{"issue":"5","key":"9695_CR34","doi-asserted-by":"publisher","first-page":"708","DOI":"10.1017\/S1471068422000242","volume":"22","author":"A Charalambidis","year":"2022","unstructured":"Charalambidis, A., Nomikos, C., Rondogiannis, P.: Strong equivalence of logic programs with ordered disjunction: A logical perspective. Theory Pract. Log. Program. 22(5), 708\u2013722 (2022)","journal-title":"Theory Pract. Log. Program."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09695-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09695-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09695-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,22]],"date-time":"2024-06-22T07:08:28Z","timestamp":1719040108000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09695-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,3]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["9695"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09695-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,3]]},"assertion":[{"value":"23 January 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 February 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 April 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"8"}}