Sequent Calculi for Choice Logics

Michael Bernreiter; Anela Lolic; Jan Maly; Stefan Woltran

doi:10.1007/978-3-031-10769-6_20

Sequent Calculi for Choice Logics

Michael Bernreiter^*, Anela Lolic, Jan Maly, Stefan Woltran

^*Corresponding author for this work

Publication: Chapter in book/Conference proceeding › Contribution to conference proceedings

Abstract

Choice logics constitute a family of propositional logics and are used for the representation of preferences, with especially qualitative choice logic (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 F is entailed by a QCL-theory T if F is true in all preferred models of T. 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 conjunctive choice logic (CCL) can be obtained in a straightforward way.

Original language	English
Title of host publication	Automated Reasoning
Subtitle of host publication	11th International Joint Conference Proceedings (IJCAR 2022)
Editors	Jasmin Blanchette, Laura Kovács, Dirk Pattinson
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	331-349
Number of pages	19
ISBN (Print)	9783031107689
DOIs	https://doi.org/10.1007/978-3-031-10769-6_20
Publication status	Published - 2022
Externally published	Yes
Event	11th International Joint Conference on Automated Reasoning, IJCAR 2022, part of the Federated Logic Conference, FLoC 2022 - Haifa, Israel Duration: 8 Aug 2022 → 10 Aug 2022

Publication series

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13385 LNAI
ISSN	0302-9743

Conference

Conference	11th International Joint Conference on Automated Reasoning, IJCAR 2022, part of the Federated Logic Conference, FLoC 2022
Country/Territory	Israel
City	Haifa
Period	8/08/22 → 10/08/22

Bibliographical note

Publisher Copyright:
© 2022, The Author(s).

Access to Document

10.1007/978-3-031-10769-6_20Licence: CC BY

Check availability

University Library Catalogue

Cite this

Bernreiter, Michael ; Lolic, Anela ; Maly, Jan et al. / Sequent Calculi for Choice Logics. Automated Reasoning: 11th International Joint Conference Proceedings (IJCAR 2022). editor / Jasmin Blanchette ; Laura Kovács ; Dirk Pattinson. Springer Science and Business Media Deutschland GmbH, 2022. pp. 331-349 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13385 LNAI).

@inproceedings{3bcd6987bc2248afa277104def5330bf,

title = "Sequent Calculi for Choice Logics",

abstract = "Choice logics constitute a family of propositional logics and are used for the representation of preferences, with especially qualitative choice logic (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 F is entailed by a QCL-theory T if F is true in all preferred models of T. 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 conjunctive choice logic (CCL) can be obtained in a straightforward way.",

author = "Michael Bernreiter and Anela Lolic and Jan Maly and Stefan Woltran",

note = "Publisher Copyright: {\textcopyright} 2022, The Author(s).; 11th International Joint Conference on Automated Reasoning, IJCAR 2022, part of the Federated Logic Conference, FLoC 2022 ; Conference date: 08-08-2022 Through 10-08-2022",

year = "2022",

doi = "10.1007/978-3-031-10769-6_20",

language = "English",

isbn = "9783031107689",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "331--349",

editor = "Jasmin Blanchette and Laura Kov{\'a}cs and Dirk Pattinson",

booktitle = "Automated Reasoning",

address = "Germany",

}

Bernreiter, M, Lolic, A, Maly, J & Woltran, S 2022, Sequent Calculi for Choice Logics. in J Blanchette, L Kovács & D Pattinson (eds), Automated Reasoning: 11th International Joint Conference Proceedings (IJCAR 2022). Springer Science and Business Media Deutschland GmbH, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13385 LNAI, pp. 331-349, 11th International Joint Conference on Automated Reasoning, IJCAR 2022, part of the Federated Logic Conference, FLoC 2022, Haifa, Israel, 8/08/22. https://doi.org/10.1007/978-3-031-10769-6_20

Sequent Calculi for Choice Logics. / Bernreiter, Michael; Lolic, Anela; Maly, Jan et al.
Automated Reasoning: 11th International Joint Conference Proceedings (IJCAR 2022). ed. / Jasmin Blanchette; Laura Kovács; Dirk Pattinson. Springer Science and Business Media Deutschland GmbH, 2022. p. 331-349 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13385 LNAI).

Publication: Chapter in book/Conference proceeding › Contribution to conference proceedings

TY - GEN

T1 - Sequent Calculi for Choice Logics

AU - Bernreiter, Michael

AU - Lolic, Anela

AU - Maly, Jan

AU - Woltran, Stefan

PY - 2022

Y1 - 2022

N2 - Choice logics constitute a family of propositional logics and are used for the representation of preferences, with especially qualitative choice logic (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 F is entailed by a QCL-theory T if F is true in all preferred models of T. 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 conjunctive choice logic (CCL) can be obtained in a straightforward way.

AB - Choice logics constitute a family of propositional logics and are used for the representation of preferences, with especially qualitative choice logic (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 F is entailed by a QCL-theory T if F is true in all preferred models of T. 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 conjunctive choice logic (CCL) can be obtained in a straightforward way.

U2 - 10.1007/978-3-031-10769-6_20

DO - 10.1007/978-3-031-10769-6_20

M3 - Contribution to conference proceedings

AN - SCOPUS:85135796818

SN - 9783031107689

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 331

EP - 349

BT - Automated Reasoning

A2 - Blanchette, Jasmin

A2 - Kovács, Laura

A2 - Pattinson, Dirk

PB - Springer Science and Business Media Deutschland GmbH

T2 - 11th International Joint Conference on Automated Reasoning, IJCAR 2022, part of the Federated Logic Conference, FLoC 2022

Y2 - 8 August 2022 through 10 August 2022

ER -

Bernreiter M, Lolic A, Maly J, Woltran S. Sequent Calculi for Choice Logics. In Blanchette J, Kovács L, Pattinson D, editors, Automated Reasoning: 11th International Joint Conference Proceedings (IJCAR 2022). Springer Science and Business Media Deutschland GmbH. 2022. p. 331-349. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13385 LNAI). doi: 10.1007/978-3-031-10769-6_20