{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T03:02:12Z","timestamp":1760238132992,"version":"build-2065373602"},"reference-count":67,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2020,7,21]],"date-time":"2020-07-21T00:00:00Z","timestamp":1595289600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Axioms"],"abstract":"<jats:p>Default logic is one of the basic formalisms for nonmonotonic reasoning, a well-established area from logic-based artificial intelligence dealing with the representation of rational conclusions, which are characterised by the feature that the inference process may require to retract prior conclusions given additional premisses. This nonmonotonic aspect is in contrast to valid inference relations, which are monotonic. Although nonmonotonic reasoning has been extensively studied in the literature, only few works exist dealing with a proper proof theory for specific logics. In this paper, we introduce sequent-type calculi for two variants of default logic, viz., on the one hand, for three-valued default logic due to Radzikowska, and on the other hand, for disjunctive default logic, due to Gelfond, Lifschitz, Przymusinska, and Truszczy\u0144ski. The first variant of default logic employs \u0141ukasiewicz\u2019s three-valued logic as the underlying base logic and the second variant generalises defaults by allowing a selection of consequents in defaults. Both versions have been introduced to address certain representational shortcomings of standard default logic. The calculi we introduce axiomatise brave reasoning for these versions of default logic, which is the task of determining whether a given formula is contained in some extension of a given default theory. Our approach follows the sequent method first introduced in the context of nonmonotonic reasoning by Bonatti, which employs a rejection calculus for axiomatising invalid formulas, taking care of expressing the consistency condition of defaults.<\/jats:p>","DOI":"10.3390\/axioms9030084","type":"journal-article","created":{"date-parts":[[2020,7,22]],"date-time":"2020-07-22T03:23:16Z","timestamp":1595388196000},"page":"84","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Sequent-Type Calculi for Three-Valued and Disjunctive Default Logic"],"prefix":"10.3390","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2247-8147","authenticated-orcid":false,"given":"Sopo","family":"Pkhakadze","sequence":"first","affiliation":[{"name":"Knowledge-Based System Group, Institut f\u00fcr Logic and Computation, Technische Universit\u00e4t Wien, Favoritenstra\u00dfe 9-11, 1040 Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5673-2460","authenticated-orcid":false,"given":"Hans","family":"Tompits","sequence":"additional","affiliation":[{"name":"Knowledge-Based System Group, Institut f\u00fcr Logic and Computation, Technische Universit\u00e4t Wien, Favoritenstra\u00dfe 9-11, 1040 Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2020,7,21]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/0004-3702(80)90014-4","article-title":"A Logic for Default Reasoning","volume":"13","author":"Reiter","year":"1980","journal-title":"Artif. Intell."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0004-3702(85)90042-6","article-title":"Semantical Considerations on Nonmonotonic Logic","volume":"25","author":"Moore","year":"1985","journal-title":"Artif. Intell."},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0004-3702(80)90011-9","article-title":"Circumscription\u2014A Form of Non-Monotonic Reasoning","volume":"13","author":"McCarthy","year":"1980","journal-title":"Artif. Intell."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/BF03037169","article-title":"Classical Negation in Logic Programs and Disjunctive Databases","volume":"9","author":"Gelfond","year":"1991","journal-title":"New Gener. Comput."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10472-006-9028-z","article-title":"Equilibrium Logic","volume":"47","author":"Pearce","year":"2006","journal-title":"Ann. Math. Artif. Intell."},{"key":"ref_6","unstructured":"Haugeland, J. (1975). A Framework for Representing Knowledge. Mind Design, MIT Press."},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/3-540-61208-4_9","article-title":"Sequent Calculi for Default and Autoepistemic Logic","volume":"Volume 1071","author":"Miglioli","year":"1996","journal-title":"Proceedings of the 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX \u201996), Lecture Notes in Computer Science"},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1145\/505372.505374","article-title":"Sequent Calculi for Propositional Nonmonotonic Logics","volume":"3","author":"Bonatti","year":"2002","journal-title":"ACM Trans. Comput. Log."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1080\/11663081.1996.10510876","article-title":"A Three-Valued Approach to Default Logic","volume":"6","author":"Radzikowska","year":"1996","journal-title":"J. Appl. Non-Class. Logics"},{"key":"ref_10","unstructured":"Allen, J.F., Fikes, R., and Sandewall, E. (1991, January 22\u201325). Disjunctive Defaults. Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR\u201991), Cambridge, MA, USA."},{"key":"ref_11","first-page":"51","article-title":"Philosophische Bemerkungen zu mehrwertigen Systemen des Aussagenkalk\u00fcls","volume":"23","year":"1930","journal-title":"Comptes Rendus Des S\u00e9ances De La Soci\u00e9t\u00e9 Des Sciences Et Des Lettres De Varsovie Cl III"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1111\/j.1467-8640.1988.tb00086.x","article-title":"Considerations on Default Logic\u2014An alternative approach","volume":"4","year":"1988","journal-title":"Comput. Intell."},{"key":"ref_13","unstructured":"Schaub, T. (1992). On Constrained Default Theories, FG Intellektik, FB Informatik, TH Darmstadt. Technical Report AIDA-92-2."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/0004-3702(94)90106-6","article-title":"Alternative Approaches to Default Logic","volume":"70","author":"Delgrande","year":"1994","journal-title":"Artif. Intell."},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Pereira, L.M., and Nerode, A. (1993, January 28\u201330). Rational Default Logic and Disjunctive Logic Programming. Proceedings of the 2nd International Workshop on Logic Programming and Non-Monotonic Reasoning (LPNMR\u201993), Lisbon, Portugal.","DOI":"10.7551\/mitpress\/4307.001.0001"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s10472-009-9161-6","article-title":"General Default Logic","volume":"57","author":"Zhou","year":"2009","journal-title":"Ann. Math. Artif. Intell."},{"key":"ref_17","first-page":"195","article-title":"Four-Valued Semantics for Default Logic","volume":"Volume 4013","author":"Lamontagne","year":"2006","journal-title":"Proceedings of the 19th Conference of the Canadian Society for Computational Studies of Intelligence (Canadian AI 2006), Lecture Notes in Computer Science"},{"key":"ref_18","unstructured":"Gabbay, D., and Woods, J. (2007). Default Logic. Handbook of the History of Logic, Volume 8: The Many Valued and Nonmonotonic Turn in Logic, North-Holland."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1093\/logcom\/exq061","article-title":"The Complexity of Reasoning for Fragments of Default Logic","volume":"22","author":"Beyersdorff","year":"2012","journal-title":"J. Log. Comput."},{"key":"ref_20","first-page":"220","article-title":"O sylogistyce Arystotelesa","volume":"44","year":"1939","journal-title":"Sprawozdania Z Czynno\u015bci I Posiedze\u0144 Polskiej Akademii Umiej\u0119tno\u015bci"},{"key":"ref_21","first-page":"89","article-title":"A Sequent Calculus for Lukasiewicz\u2019s Three-Valued Logic Based on Suszko\u2019s Bivalent Semantics","volume":"28","year":"1999","journal-title":"Bull. Sect. Log."},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Fitting, M., and Or\u0142owska, E. (2003). Classical Gentzen-Type Methods in Propositional Many-Valued Logics. Beyond Two: Theory and Applications in Multiple-Valued Logics, Springer.","DOI":"10.1007\/978-3-7908-1769-0"},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen I","volume":"39","author":"Gentzen","year":"1935","journal-title":"Math. Z."},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"276","DOI":"10.2307\/2274919","article-title":"Natural 3-Valued Logics\u2014Characterization and Proof Theory","volume":"56","author":"Avron","year":"1991","journal-title":"J. Symb. Log."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"23","DOI":"10.4064\/fm-60-1-23-33","article-title":"Sequents in Many Valued Logic I","volume":"60","author":"Rousseau","year":"1967","journal-title":"Fundam. Math."},{"key":"ref_26","unstructured":"Zach, R. (1993). Proof Theory of Finite-Valued Logics. [Master\u2019s Thesis, Technische Universit\u00e4t Wien, Institut f\u00fcr Computersprachen]."},{"key":"ref_27","unstructured":"Urba\u0144ski, M., Skura, T., and \u0141upkowski, P. (2020). On Sequent-Type Rejection Calculi for Many-Valued Logics. Reasoning: Games, Cognition, Logic, College Publications."},{"key":"ref_28","first-page":"189","article-title":"Logika dwuwarto\u015bciowa","volume":"23","year":"1921","journal-title":"Przegl\u0105d Filozoficzny"},{"key":"ref_29","unstructured":"\u0141ukasiewicz, J. (1957). Aristotle\u2019s Syllogistic from the Standpoint of Modern Formal Logic, Clarendon Press. [2nd ed.]."},{"key":"ref_30","unstructured":"S\u0142upecki, J. (1948). Z Bada\u0144 Nad Sylogistyk\u0105 Arystotelesa, Wroc\u0142awskie Towarzystwo Naukowe."},{"key":"ref_31","first-page":"33","article-title":"Funkcja \u0141ukasiewieza","volume":"3","year":"1959","journal-title":"Zesz. Nauk. Uniw. Wroc\u0142awskiego Ser. A"},{"key":"ref_32","first-page":"5","article-title":"Teoria zda\u0144 odrzuconych","volume":"22","year":"1969","journal-title":"Zesz. Nauk. Wy\u017cszej Szko\u0142y Pedagog. W Opolu Ser. B Stud. I Monogr."},{"key":"ref_33","first-page":"133","article-title":"Kilka uzupelnie\u0144 teorii zda\u0144 odrzuconych","volume":"22","author":"Bryll","year":"1969","journal-title":"Zesz. Nauk. Wy\u017cszej Szko\u0142y Pedagog. W Opolu Ser. B Stud. I Monogr."},{"key":"ref_34","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BF02121863","article-title":"Theory of Rejected Propositions I","volume":"29","author":"Bryll","year":"1971","journal-title":"Stud. Log."},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/BF02120839","article-title":"Theory of Rejected Propositions II","volume":"30","author":"Bryll","year":"1972","journal-title":"Stud. Log."},{"key":"ref_36","doi-asserted-by":"crossref","unstructured":"Tiomkin, M.L. (1988, January 5\u20138). Proving Unprovability. Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS\u201988), Scotland, UK.","DOI":"10.1109\/LICS.1988.5097"},{"key":"ref_37","unstructured":"Bonatti, P.A. (1993). A Gentzen System for Non-Theorems, Christian Doppler Labor f\u00fcr Expertensysteme, Technische Universit\u00e4t Wien. Technical Report CD-TR 93\/52."},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/BF01054714","article-title":"Refutation Systems in Modal Logic","volume":"53","author":"Goranko","year":"1994","journal-title":"Stud. Log."},{"key":"ref_39","first-page":"75","article-title":"A Complete Syntactic Characterization of the Intuitionistic Logic","volume":"23","author":"Skura","year":"1989","journal-title":"Rep. Math. Log."},{"key":"ref_40","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1007\/BF00370199","article-title":"The Method of Axiomatic Rejection for the Intuitionistic Propositional Logic","volume":"48","author":"Dutkiewicz","year":"1989","journal-title":"Stud. Log."},{"key":"ref_41","unstructured":"Behara, M., Fritsch, R., and Lintz, R.G. (1995). Loop-Free Construction of Counter-Models for Intuitionistic Propositional Logic. Symposia Gaussiana, Proceedings of the 2nd Gauss Symposium, Conference A: Mathematics and Theoretical Physics, Munich, Germany, 2\u20137 August 1993, Walter de Gruyter."},{"key":"ref_42","first-page":"1","article-title":"Aspects of Refutation Procedures in the Intuitionistic Logic and Related Modal Systems","volume":"20","author":"Skura","year":"1999","journal-title":"Acta Univ. Wratislav. Log."},{"key":"ref_43","first-page":"115","article-title":"Refutation Systems in Propositional Logic","volume":"Volume 16","author":"Gabbay","year":"2011","journal-title":"Handbook of Philosophical Logic"},{"key":"ref_44","unstructured":"Skura, T. (2013). Refutation Methods in Modal Propositional Logic, Semper."},{"key":"ref_45","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/978-3-319-08909-6_5","article-title":"On Axiomatic Rejection for the Description Logic ALC","volume":"Volume 8439","author":"Berger","year":"2014","journal-title":"Declarative Programming and Knowledge Management\u2013Declarative Programming Days (KDPD 2013)"},{"key":"ref_46","first-page":"179","article-title":"On the Notion and Function of the Rejection of Propositions","volume":"23","year":"2005","journal-title":"Acta Univ. Wratislav. Log."},{"key":"ref_47","unstructured":"Rosser, J.B., and Turquette, A.R. (1952). Many-Valued Logics, North-Holland."},{"key":"ref_48","unstructured":"Gabbay, D., and Woods, J. (2007). Many-Valued Logic and its Philosophy. Handbook of the History of Logic, Volume 8: The Many Valued and Nonmonotonic Turn in Logic, North-Holland."},{"key":"ref_49","first-page":"136","article-title":"Aksjomatyzacja tr\u00f3jwarto\u015bciowego rachunku zda\u0144","volume":"24","author":"Wajsberg","year":"1931","journal-title":"Comptes Rendus Des S\u00e9ances De La Soci\u00e9t\u00e9 Des Sciences Et Des Lettres De Varsovie Cl III"},{"key":"ref_50","unstructured":"\u0141ukaszewicz, W. (1990). Non-Monotonic Reasoning: Formalization of Commonsense Reasoning, Ellis Horwood."},{"key":"ref_51","doi-asserted-by":"crossref","unstructured":"Pearl, J. (1988). Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference, Morgan Kaufmann Publishers.","DOI":"10.1016\/B978-0-08-051489-5.50008-4"},{"key":"ref_52","unstructured":"Brachman, R.J., Levesque, H.J., and Reiter, R. (1989, January 15\u201318). What the Lottery Paradox Tells us about Default Reasoning. Proceedings of the First International Conference on Principles of Knowledge Representation and Reasoning (KR\u201989), Toronto, ON, Canada."},{"key":"ref_53","unstructured":"Parikh, R. (1990, January 4\u20137). Epistemic Semantics for Fixed-Points Non-Monotonic Logics. Proceedings of the Third Conference on Theoretical Aspects of Reasoning about Knowledge (TARK\u201990), Pacific Grove, CA, USA."},{"key":"ref_54","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1016\/S0304-3975(01)00383-8","article-title":"Propositional Default Logics Made Easier: Computational Complexity of Model Checking","volume":"289","author":"Baumgartner","year":"2002","journal-title":"Theor. Comput. Sci."},{"key":"ref_55","unstructured":"Bonatti, P.A. (1993). Sequent Calculi for Default and Autoepistemic Logic, Christian Doppler Labor f\u00fcr Expertensysteme, Technische Universit\u00e4t Wien. Technical Report CD-TR 93\/53."},{"key":"ref_56","first-page":"59","article-title":"On Sequents and Tableaux for Many-Valued Logics","volume":"8","author":"Carnielli","year":"1991","journal-title":"J. Non-Class. Log."},{"key":"ref_57","doi-asserted-by":"crossref","unstructured":"Avron, A. (1996). The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logics. Logic: From Foundations to Applications, Clarendon Press.","DOI":"10.1093\/oso\/9780198538622.003.0001"},{"key":"ref_58","doi-asserted-by":"crossref","unstructured":"D\u2019Agostino, M., Gabbay, D., H\u00e4hnle, R., and Posegga, J. (1999). Tableaux for Many-Valued Logics. Handbook of Tableaux Methods, Kluwer.","DOI":"10.1007\/978-94-017-1754-0"},{"key":"ref_59","doi-asserted-by":"crossref","unstructured":"Marek, W., and Truszczy\u0144ski, M. (1993). Nonmonotonic Logic: Context-Dependent Reasoning, Springer.","DOI":"10.1007\/978-3-662-02906-0"},{"key":"ref_60","unstructured":"Egly, U., and Tompits, H. (1997, January 17\u201319). A Sequent Calculus for Intuitionistic Default Logic. Proceedings of the 12th Workshop on Logic Programming (WLP\u201997), Forschungsbericht PMS-FB-1997-10, Institut f\u00fcr Informatik, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Munich, Germany."},{"key":"ref_61","doi-asserted-by":"crossref","unstructured":"Lupea, M. (2008, January 26\u201329). Axiomatization of Credulous Reasoning in Default Logics using Sequent Calculus. Proceedings of the 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2008), Timisoara, Romania.","DOI":"10.1109\/SYNASC.2008.43"},{"key":"ref_62","unstructured":"Wahlster, W. (1996, January 11\u201316). Implementing Circumscription Using a Tableau Method. Proceedings of the 12th European Conference on Artificial Intelligence (ECAI\u201996), Budapest, Hungary."},{"key":"ref_63","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1093\/logcom\/6.2.205","article-title":"A Proof Theoretical Approach to Default Reasoning I: Tableaux for Default Logic","volume":"6","author":"Amati","year":"1996","journal-title":"J. Log. Comput."},{"key":"ref_64","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/10722086_28","article-title":"A Tableau Calculus for Equilibrium Entailment","volume":"Volume 1847","author":"Dyckhoff","year":"2000","journal-title":"Proceedings of the 9th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000), Lecture Notes in Computer Science"},{"key":"ref_65","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/s10472-007-9075-0","article-title":"Partial Equilibrium Logic","volume":"50","author":"Cabalar","year":"2007","journal-title":"Ann. Math. Artif. Intell."},{"key":"ref_66","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2480759.2480767","article-title":"Tableau Calculi for Logic Programs under Answer Set Semantics","volume":"14","author":"Gebser","year":"2013","journal-title":"ACM Trans. Comput. Log."},{"key":"ref_67","first-page":"254","article-title":"Gentzen-Type Refutation Systems for Three-Valued Logics with an Application to Disproving Strong Equivalence","volume":"Volume 6645","author":"Delgrande","year":"2011","journal-title":"Proceedings of the 11th International Conference on Logic Programming and Nonmonotonic Resoning (LPNMR 2011), Lecture Notes in Computer Science"}],"container-title":["Axioms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2075-1680\/9\/3\/84\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T09:50:25Z","timestamp":1760176225000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2075-1680\/9\/3\/84"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,21]]},"references-count":67,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2020,9]]}},"alternative-id":["axioms9030084"],"URL":"https:\/\/doi.org\/10.3390\/axioms9030084","relation":{},"ISSN":["2075-1680"],"issn-type":[{"type":"electronic","value":"2075-1680"}],"subject":[],"published":{"date-parts":[[2020,7,21]]}}}