Abstract
We build a Default Logic variant on Intuitionistic Propositional Logic and develop a sound, complete, and terminating, tableaux calculus for it. We also present an implementation of the calculus. We motivate and illustrate the technical elements of our work with examples.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
This notion is referred to as local consequence in the literature on Modal Logic.
- 2.
This notion is referred to as sceptical consequence in the literature on Default Logics.
- 3.
The ‘@’ notation is borrowed from Hybrid Logic [3].
- 4.
The signs \(+\) and − are necessary since in \(\mathsf {IPL}\) we cannot use the symbol \(\lnot \) of negation for expressing that a formula does not hold in a world.
References
Amati, G., Aiello, L., Gabbay, D., Pirri, F.: A proof theoretical approach to default reasoning I: tableaux for default logic. J. Log. Comput. 6(2), 205–231 (1996)
Antoniou, G.: Nonmonotonic Reasoning. The MIT Press, Cambridge (1997)
Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, et al. [4], pp. 821–868
Blackburn, P., van Benthem, J., Wolter, F. (eds.): Handbook of Modal Logic. Elsevier, Amsterdam (2007)
Bochman, A.: Non-monotonic reasoning. In: Gabbay and Woods [20], pp. 555–632
Brewka, G.: Cumulative default logic: in defense of nonmonotonic inference rules. Artif. Intell. 50(2), 183–205 (1991)
Cassano, V., Areces, C., Castro, P.: Reasoning about prescription and description using prioritized default rules. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-22), EPiC Series in Computing, vol. 57, pp. 196–213. EasyChair (2018)
Cassano, V., Fervari, R., Areces, C., Castro, P.F.: Interpolation and beth definability in default logics. In: Calimeri, F., Leone, N., Manna, M. (eds.) JELIA 2019. LNCS (LNAI), vol. 11468, pp. 675–691. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-19570-0_44
Cassano, V., Pombo, C.G.L., Maibaum, T.S.E.: A propositional tableaux based proof calculus for reasoning with default rules. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 6–21. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24312-2_2
Cholewinski, P., Marek, V., Truszczynski, M.: Default reasoning system DeReS. In: 5th International Conference on Principles of Knowledge Representation and Reasoning (KR 1996), pp. 518–528. Morgan Kaufmann (1996)
Claessen, K., Rosén, D.: SAT modulo intuitionistic implications. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 622–637. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48899-7_43
Delgrande, J., Schaub, T., Jackson, W.: Alternative approaches to default logic. Artif. Intell. 70(1–2), 167–237 (1994)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_37
Egly, U., Tompits, H.: A sequent calculus for intuitionistic default logic. In: 12th Workshop Logic Programming (WLP 1997), pp. 69–79 (1997)
Ferrari, M., Fiorentini, C., Fiorino, G.: A tableau calculus for propositional intuitionistic logic with a refined treatment of nested implications. J. Appl. Non-Class. Log. 19, 149–166 (2009)
Ferrari, M., Fiorentini, C., Fiorino, G.: fCube: an efficient prover for intuitionistic propositional logic. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 294–301. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16242-8_21
Fitting, M.: Proof Methods for Modal and Intuitionistic Logics. Springer, Dordrecht (1983). https://doi.org/10.1007/978-94-017-2794-5
Font, J.: Abstract Algebraic Logic: An Introductory Textbook, 1st edn. College Publications (2016)
Gabbay, D.M.: Intuitionistic basis for non-monotonic logic. In: Loveland, D.W. (ed.) CADE 1982. LNCS, vol. 138, pp. 260–273. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0000064
Gabbay, D., Woods, J. (eds.): Handbook of the History of Logic: The Many Valued and Nonmonotonic Turn in Logic, vol. 8. North-Holland, Amsterdam (2007)
Goré, R., Thomson, J., Wu, J.: A history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 262–268. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_19
Haeusler, E., de Paiva, V., Rademaker, A.: Intuitionistic logic and legal ontologies. In: 23rd International Conference on Legal Knowledge and Information Systems (JURIX 2010), Frontiers in Artificial Intelligence and Applications, vol. 223, pages 155–158. IOS Press (2010)
Hughes, G., Cresswell, M.: An Introduction to Modal Logic. Methuen, London (1968)
Hustadt, U., Schmidt, R.A.: Simplification and backjumping in modal tableau. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 187–201. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-69778-0_22
Kaminski, M., Smolka, G.: Terminating tableau systems for hybrid logic with difference and converse. J. Log. Lang. Inf. 18(4), 437–464 (2009)
Kapsner, A.: The logic of guilt, innocence and legal discourse. In: Urbaniak, R., Payette, G. (eds.) Applications of Formal Philosophy. LARI, vol. 14, pp. 7–24. Springer, Cham (2017)
Łukaszewicz, W.: Considerations on default logic: an alternative approach. Comput. Intell. 4, 1–16 (1988)
Makinson, D., van der Torre, L.: What is input/output logic? Input/output logic, constraints, permissions. In: Boella, G., van der Torre, L., Verhagen, H. (eds.) Normative Multi-agent Systems, Dagstuhl Seminar Proceedings, vol. 07122. Internationales Begegnungsund Forschungszentrum für Informatik (2007)
Mikitiuk, A., Truszczynski, M.: Constrained and rational default logics. In: 14th International Joint Conference on Artificial Intelligence (IJCAI 1995), pp. 1509–1517 (1995)
Osorio, M., Navarro Pérez, J., Arrazola, J.: Applications of intuitionistic logic in answer set programming. TPLP 4(3), 325–354 (2004)
Parent, X., Gabbay, D., Torre, L.: Intuitionistic basis for input/output logic. In: Hansson, S.O. (ed.) David Makinson on Classical Methods for Non-Classical Problems. OCL, vol. 3, pp. 263–286. Springer, Dordrecht (2014). https://doi.org/10.1007/978-94-007-7759-0_13
Pearce, D.: Stable inference as intuitionistic validity. J. Log. Program. 38(1), 79–91 (1999)
Pearce, D., Sarsakov, V., Schaub, T., Tompits, H., Woltran, S.: A polynomial translation of logic programs with nested expressions into disjunctive logic programs: preliminary report. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 405–420. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45619-8_28
Poole, D.: What the lottery paradox tells us about default reasoning. In: 1st International Conference on Principles of Knowledge Representation and Reasoning (KR 1989), pp. 333–340 (1989)
Priest, G.: An Introduction to Non-Classical Logic: From If to Is. Cambridge University Press, Cambridge (2000)
Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic. J. Autom. Reason. 38(1–3), 261–271 (2007)
Reiter, R.: A logic for default reasoning. Artif. Intell. 13(1–2), 81–132 (1980)
Servi, G.: Nonmonotonic consequence based on intuitionistic logic. J. Symb. Log. 57(4), 1176–1197 (1992)
Wansing, H.: Semantics-based nonmonotonic inference. Notre Dame J. Formal Log. 36(1), 44–54 (1995)
Ackowledgements
This work was partially supported by ANPCyT-PICTs-2017-1130 and 2016-0215, MinCyT Córdoba, SeCyT-UNC, the Laboratoire International Associé INFINIS and the European Union’s Horizon 2020 research and innovation programme under the Marie Skodowska-Curie grant agreement No. 690974 for the project MIREL: MIning and REasoning with Legal texts.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Cassano, V., Fervari, R., Hoffmann, G., Areces, C., Castro, P.F. (2019). A Tableaux Calculus for Default Intuitionistic Logic. In: Fontaine, P. (eds) Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science(), vol 11716. Springer, Cham. https://doi.org/10.1007/978-3-030-29436-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-29436-6_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-29435-9
Online ISBN: 978-3-030-29436-6
eBook Packages: Computer ScienceComputer Science (R0)