Multi-Agent Dialogues and Dialogue Sequents for Proof Search and Scheduling in Intuitionistic Logic and the Modal Logic S4

• Autorzy: Sticht M.

Identyfikatory

DOI

10.3233/FI-2018-1700

• Konferencja: Italian Conference on Computational Logic (Convegno Italiano di Logica Computazionale, CILC 2016) (31; 20-22.07.2016; Università degli Studi di Milano-Bicocca, Italy)
• Języki publikacji: EN

Abstrakty

EN

Dialogical games as introduced by Lorenzen and Lorenz describe a reasoning technique for intuitionistic and classical predicate logic: two players (proponent and opponent) argue about the validity of a given formula according to predefined rules. If the proponent has a winning strategy then the formula is proven to be valid. The underlying game rules can be modified to have an impact on proof search strategies and increase the efficiency of such a searching process. In this paper, a multi-agent version of dialogical logic is introduced that corresponds more to multiconclusion sequent calculi for propositional intuitionistic logic rather than single-conclusion ones which are more related to two-player dialogues. We also consider an extension for the normal modal logic S4. The rules lead us to a normalization of a proof, let us focus on the proponents' relevant decisions, and therefore give explicit directives that increase compactness of the proofsearching process. This allows us to perform parts of the proof in a parallel way. We prove soundness and completeness of these multi-agent systems.

Słowa kluczowe

EN

dialogue; proof search; intuitionistic logic; modal logic; game theories; parallel reasoning

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 161, nr 1/2
• Strony: 191--218
• Opis fizyczny: Bibliogr. 48 poz., rys., tab.

Twórcy

autor

Sticht M.

• Informatics Theory Group University of Bamberg, Germany

Bibliografia

• [1] Lorenzen P. Logik und Agon. In: Atti del XII Congresso Internazionale di Filosofia, volume 4. 1958 pp. 187-194. Reprinted in [7].
• [2] Lorenzen P. Ein dialogisches Konstruktivitätskriterium. In: Infinistic Methods. Proceeding of the Symposium on Foundations of Mathematics. 1961 pp. 193-200. Reprinted in [7].
• [3] Mann AL, Sandu G, Sevenster M. Independence-Friendly Logic - A Game-Theoretic Approach. London Mathematical Society lecture note series. Cambridge Univ. Press, 2011. ISBN-13: 978-0521149341, 10: 0521149347.
• [4] Hintikka J. Logic, language-games and information: Kantian themes in the philosophy of logic. Oxford Univ Press, 1973. ISBN-13: 978-0198243649, 10: 0198243642.
• [5] Abramsky S. A Compositional Game Semantics for Multi-Agent Logics of Partial Information. In: van Benthem J, Gabbay D, Löwe B (eds.), Interactive Logic. Amsterdam University Press, 2007 pp. 11-47.
• [6] Lorenz K. Arithmetik und Logik als Spiele. PhD thesis, Christian-Albrechts-Universität zu Kiel, 1961. Excerpts reprinted in [7].
• [7] Lorenzen P, Lorenz K. Dialogische Logik. Wissenschaftliche Buchgesellschaft, 1978.
• [8] Galmiche D, Larchey-Wendling D, Vidal-Rosset J. Some Remarks on Relations between Proofs and Games. In: Construction - Festschrift for Gerhard Heinzmann, pp. 339-357. College Publications, 2010.
• [9] Rahman S, Keiff L. On How to Be a Dialogician. In: Vanderveken D (ed.), Logic, Thought and Action, volume 2 of Logic, Epistemology, and the Unity of Science, pp. 359-408. Springer Netherlands. ISBN 978-1-4020-2616-4, 2005. doi:10.1007/1-4020-3167-X\_17.
• [10] Alama J. Dialogues for proof search. In: Benzmüller C, Otten J (eds.), ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics, volume 33 of EPiC Series in Computing. 2015 pp. 65-70. URL https://easychair.org/publications/paper/Q5SW.
• [11] Lorenzen P. Normative Logic and Ethics. Bibliographisches Institut, 1969. URL https://books.google.pl/books?id=tG5hQgAACAAJ.
• [12] Krabbe EC. Studies in Dialogical Logic. PhD thesis, Rijksuniversiteit te Groningen, 1982.
• [13] Van Dun F. On the modes of opposition in the formal dialogues of P. Lorenzen. Logique et analyse, 1972. 15:103-136.
• [14] Krabbe EC. A theory of modal dialectics. Journal of Philosophical Logic, 1986. 15(2):191-217.
• [15] Rahman S, Rückert H. Dialogische Modallogik (für T, B, S4, und S5). Logique et analyse, 1999.167(168):243-282. URL http://www.jstor.org/stable/44084659.
• [16] Clerbout N. Étude sur quelques sémantiques dialogiques: concepts fondamentaux et éléments de metathéorie. PhD thesis, Leiden University, 2013.
• [17] Lorenz K. Dialogspiele als semantische Grundlage von Logikkalkülen. Springer, 1968. Reprinted in [7]. doi:10.1007/BF01973341.
• [18] Fermüller CG. Parallel dialogue games and hypersequents for intermediate logics. In: Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX 2003, Rome, Italy, September 2003. Proceedings. Springer Berlin Heidelberg, 2003 pp. 48-64. doi:10.1007/978-3-540-45206-5_7.
• [19] Fermüller CG, Ciabattoni A. From Intuitionistic Logic to Gödel-Dummett Logic via Parallel Dialogue Games. In: In Proceedings of the 33rd IEEE International Symposium on Multiple-Valued Logic. 2003 pp. 188-193. doi:10.1109/ISMVL.2003.1201405.
• [20] Andreoli JM. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 1992. 2(3):297-347. doi:10.1093/logcom/2.3.297.
• [21] Sticht M. Multi-Agent Dialogue Games and Dialogue Sequents for Proof Search and Scheduling. In: Fiorentini C, Momigliano A (eds.), Proceedings of the 31st Italian Conference on Computational Logic. 2016 pp. 21-36. URL http://ceur-ws.org/Vol-1645/paper_20.pdf.
• [22] Barth EM, Krabbe EC. From Axiom to Dialogue: A philosophical study of logics and argumentation. Walter de Gruyter, 1982. ISBN-3110839806, 9783110839807.
• [23] Gentzen G. Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift, 1935. 39:176-210.
• [24] Egly U, Schmitt S. On intuitionistic proof transformations, their complexity, and application to constructive program synthesis. Fundamenta Informaticae, 1999. 39(1-2):59-83. doi:10.3233/FI-1999-391204.
• [25] Maehara S. Eine Darstellung der intuitionistischen Logik in der klassischen. Nagoya mathematical journal, 1954. 7:45-64. URL https://projecteuclid.org/euclid.nmj/1118799557.
• [26] Troelstra AS, Schwichtenberg H. Basic Proof Theory. Cambridge Univ. Press, second edition, 2000. ISBN-0521779111, 9780521779111.
• [27] Avron A. Hypersequents, logical consequence and intermediate logics for concurrency. Annals of Mathematics and Artificial Intelligence, 1991. 4(3):225-248. doi:10.1007/BF01531058.
• [28] Liang C, Miller D. Focusing and polarization in intuitionistic logic. In: Computer Science Logic. Springer, 2007 pp. 451-465. doi:10.1007/978-3-540-74915-8_34.
• [29] Simmons RJ. Structural focalization. ACM Transactions on Computational Logic (TOCL), 2014. 15(3):21. doi:10.1145/2629678.
• [30] Dyckhoff R, Lengrand S. LJQ: A Strongly Focused Calculus for Intuitionistic Logic. In: Logical Approaches to Computational Barriers: Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006. Proceedings. Springer Berlin Heidelberg. ISBN 978-3-540-35468-0, 2006 pp. 173-185.
• [31] Herbelin H. Séquents qu’on calcule: de l’interprétation du calcul des séquents comme calcul de lambdatermes et comme calcul de stratégies gagnantes. PhD thesis, Université Paris-Diderot-Paris VII, 1995.
• [32] Dyckhoff R. Contraction-Free Sequent Calculi for Intuitionistic Logic. The Journal of Symbolic Logic, 1992. 57(3):795-807. URL https://doi.org/10.2307/2275431.
• [33] Dragalin AG. Mathematical Intuitionism, Introduction to Proof Theory, volume 67 of Translations of Mathematical Monographs. American Mathematical Society, 1988. Translated from the Russian [48] by E. Mendelson.
• [34] Kleene SC. Introduction to Metamathematics. North Holland, 1952.
• [35] Corsi G, Tassi G. Intuitionistic logic freed of all metarules. The Journal of Symbolic Logic, 2007. 72:1204-1218. doi:10.2178/jsl/1203350782.
• [36] Heuerding A, Seyfried M, Zimmermann H. Efficient loop-check for backward proof search in some nonclassical propositional logics. In: International Workshop on Theorem Proving with Analytic Tableaux and Related Methods. Springer, 1996 pp. 210-225. doi:10.1007/3-540-61208-4_14.
• [37] Howe JM. Two loop detection mechanisms: A comparison. In: Galmiche D (ed.), Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX’97. Springer Berlin Heidelberg, 1997 pp. 188-200. doi:/10.1007/BFb0027414.
• [38] Howe JM. Proof search issues in some non-classical logic. PhD thesis, University of St Andrews, 1998. URL http://openaccess.city.ac.uk/id/eprint/1708.
• [39] Ferrari M, Fiorentini C, Fiorino G. Contraction-Free Linear Depth Sequent Calculi for Intuitionistic Propositional Logic with the Subformula Property and Minimal Depth Counter-Models. Journal of Automated Reasoning, 2013. 51(2):129-149. doi:10.1007/s10817-012-9252-7.
• [40] Gödel K. Eine Interpretation des intuitionistischen Aussagenkalküls. Ergebnisse eines mathematischen Kolloquiums 4 39-40, 1933. Reprinted: an interpretation of the intuitionistic propositional calculus, Feferman, S, ed. Gödel Collected Works I publications 1929-1936.
• [41] Kanger S. Provability in Logic. University of Stockholm, 1957.
• [42] Negri S. Proof Analysis in Modal Logic. Journal of Philosophical Logic, 2005. 34(5):507-544. URL http://www.jstor.org/stable/30226848.
• [43] Krabbe EC. Noncumulative Dialectical Models and Formal Dialectics. Journal of Philosophical Logic, 1985. 14(2):129-168.
• [44] Plotkin G, Stirling C. A Framework for Intuitionistic Modal Logics. In: Halpern JY (ed.), Theoretical Aspects of Reasoning about Knowledge. 1986 pp. 399-406.
• [45] Simpson AK. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh, 1994. URL http://hdl.handle.net/1842/407.
• [46] Mendler M, de Paiva V. Constructive CK for contexts. Context Representation and Reasoning (CRR-2005), 2005. 13.
• [47] Bierman GM, de Paiva VCV. On an Intuitionistic Modal Logic. Studia Logica, 2000. 65(3):383-416. doi:10.1023/A:1005291931660.
• [48] Dragalin AG. Matematičeskij intuicionizm, Vvedenie v teoriju dokazatel’stv. Nauka, 1979.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).