{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T05:37:41Z","timestamp":1726033061040},"publisher-location":"Cham","reference-count":68,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030221010"},{"type":"electronic","value":"9783030221027"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-22102-7_29","type":"book-chapter","created":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T12:21:26Z","timestamp":1561465286000},"page":"610-638","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automating Automated Reasoning"],"prefix":"10.1007","author":[{"given":"Yoni","family":"Zohar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dmitry","family":"Tishkovsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Renate A.","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anna","family":"Zamansky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,1]]},"reference":[{"key":"29_CR1","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.entcs.2009.02.029","volume":"231","author":"P Abate","year":"2009","unstructured":"Abate, P., Gor\u00e9, R.: The tableau workbench. Electron. Notes Theor. Comput. Sci. 231, 55\u201367 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"6","key":"29_CR2","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1016\/S0953-5438(99)00023-5","volume":"12","author":"S Aitken","year":"2000","unstructured":"Aitken, S., Melham, T.: An analysis of errors in interactive proof attempts. Interact. Comput. 12(6), 565\u2013586 (2000)","journal-title":"Interact. Comput."},{"key":"29_CR3","unstructured":"Areces, C.E.: Logic engineering: the case of description and hybrid logics. Ph.D. thesis, University of Amsterdam (2000)"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-14128-7_13","volume-title":"Intelligent Computer Mathematics","author":"A Asperti","year":"2010","unstructured":"Asperti, A., Coen, C.S.: Some considerations on the usability of interactive provers. In: Autexier, S., et al. (eds.) CICM 2010. LNCS (LNAI), vol. 6167, pp. 147\u2013156. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14128-7_13"},{"issue":"1","key":"29_CR5","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/0890-5401(91)90023-U","volume":"92","author":"A Avron","year":"1991","unstructured":"Avron, A.: Simple consequence relations. Inf. Comput. 92(1), 105\u2013139 (1991)","journal-title":"Inf. Comput."},{"key":"29_CR6","series-title":"Studies in Fuzziness and Soft Computing","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-7908-1769-0_5","volume-title":"Beyond Two: Theory and Applications of Multiple-Valued Logic","author":"A Avron","year":"2003","unstructured":"Avron, A.: Classical Gentzen-type methods in propositional many-valued logics. In: Fitting, M., Or\u0142owska, E. (eds.) Beyond Two: Theory and Applications of Multiple-Valued Logic. Studies in Fuzziness and Soft Computing, vol. 114, pp. 117\u2013155. Physica-Verlag, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-7908-1769-0_5"},{"key":"29_CR7","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1013882326814","volume":"69","author":"F Baader","year":"2001","unstructured":"Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Stud. Logica 69, 5\u201340 (2001)","journal-title":"Stud. Logica"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-61511-3_84","volume-title":"Automated Deduction \u2014 Cade-13","author":"M Baaz","year":"1996","unstructured":"Baaz, M., Ferm\u00fcller, C.G., Salzer, G., Zach, R.: MUltlog 1.0: towards an expert system for many-valued logics. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 226\u2013230. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61511-3_84"},{"key":"29_CR9","doi-asserted-by":"publisher","unstructured":"Baumgartner, P., Schmidt, R.A.: Blocking and other enhancements for bottom-up model generation methods. J. Autom. Reason. 1\u201327 (2019). https:\/\/doi.org\/10.1007\/s10817-019-09515-1","DOI":"10.1007\/s10817-019-09515-1"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-15201-1_1","volume-title":"Software Engineering and Formal Methods","author":"B Beckert","year":"2015","unstructured":"Beckert, B., Grebing, S., B\u00f6hl, F.: A usability evaluation of interactive theorem provers using focus groups. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 3\u201319. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15201-1_1"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Caridroit, T., Lagniez, J.M., Le Berre, D., de Lima, T., Montmirail, V.: A SAT-based approach for solving the modal logic S5-satisfiability problem. In: Singh, S.P., Markovitch, S. (eds.) Thirty-First AAAI Conference on Artificial Intelligence, pp. 3864\u20133870. AAAI Press (2017)","DOI":"10.1609\/aaai.v31i1.11128"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-35722-0_9","volume-title":"Logical Foundations of Computer Science","author":"A Ciabattoni","year":"2013","unstructured":"Ciabattoni, A., Lahav, O., Spendier, L., Zamansky, A.: Automated support for the investigation of paraconsistent and other logics. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 119\u2013133. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35722-0_9"},{"issue":"1","key":"29_CR13","doi-asserted-by":"publisher","first-page":"5:1","DOI":"10.1145\/2661636","volume":"16","author":"A Ciabattoni","year":"2014","unstructured":"Ciabattoni, A., Lahav, O., Spendier, L., Zamansky, A.: Taming paraconsistent (and other) logics: an algorithmic approach. ACM Trans. Comput. Logic 16(1), 5:1\u20135:23 (2014)","journal-title":"ACM Trans. Comput. Logic"},{"key":"29_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-319-11558-0_2","volume-title":"Logics in Artificial Intelligence","author":"A Ciabattoni","year":"2014","unstructured":"Ciabattoni, A., Spendier, L.: Tools for the investigation of substructural and paraconsistent logics. In: Ferm\u00e9, E., Leite, J. (eds.) JELIA 2014. LNCS (LNAI), vol. 8761, pp. 18\u201332. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11558-0_2"},{"key":"29_CR15","unstructured":"Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Logic in Computer Science (LICS 2003), pp. 271\u2013280. IEEE Computer Society (2003)"},{"key":"29_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-2(1:5)2006","volume":"2","author":"W Conradie","year":"2006","unstructured":"Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and completeness in modal logic I: the core algorithm SQEMA. Log. Methods Comput. Sci. 2, 1\u20135 (2006)","journal-title":"Log. Methods Comput. Sci."},{"issue":"1","key":"29_CR17","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1093\/logcom\/ext021","volume":"26","author":"C Cotrini","year":"2016","unstructured":"Cotrini, C., Gurevich, Y.: Basic primal infon logic. J. Logic Comput. 26(1), 117 (2016)","journal-title":"J. Logic Comput."},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: The inverse method. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 179\u2013272. MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50006-0"},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"Dixon, C., Konev, B., Schmidt, R.A., Tishkovsky, D.: Labelled tableaux for temporal logic with cardinality constraints. In: Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012), pp. 111\u2013118. IEEE Computer Society (2012)","DOI":"10.1109\/SYNASC.2012.47"},{"issue":"3","key":"29_CR20","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1005722130532","volume":"18","author":"P Doherty","year":"1997","unstructured":"Doherty, P., \u0141ukaszewicz, W., Sza\u0142as, A.: Computing circumscription revisited: a reduction algorithm. J. Autom. Reason. 18(3), 297\u2013336 (1997)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"29_CR21","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1305\/ndjfl\/1093894722","volume":"13","author":"M Fitting","year":"1972","unstructured":"Fitting, M.: Tableau methods of proof for modal logics. Notre Dame J. Formal Logic 13(2), 237\u2013247 (1972)","journal-title":"Notre Dame J. Formal Logic"},{"key":"29_CR22","unstructured":"Gaschnig., J.: Performance measurement and analysis of certain search algorithms. Ph.D. thesis, Carnegie-Mellon University (1979)"},{"key":"29_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/11554554_25","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"O Gasquet","year":"2005","unstructured":"Gasquet, O., Herzig, A., Longin, D., Sahade, M.: LoTREC: logical tableaux research engineering companion. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 318\u2013322. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11554554_25"},{"key":"29_CR24","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G Gentzen","year":"1934","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schliessen. Mathematische Zeitschrift 39, 176\u2013210 (1934)","journal-title":"Mathematische Zeitschrift"},{"key":"29_CR25","doi-asserted-by":"crossref","unstructured":"Ginsberg, M.L., McAllester, D.A.: GSAT and dynamic backtracking. In: Doyle, J., Sandewall, E., Torasso, P. (eds.) Principles of Knowledge Representation and Reasoning (KR 1994), pp. 226\u2013237. Morgan Kaufmann (1994)","DOI":"10.1016\/B978-1-4832-1452-8.50117-2"},{"issue":"2","key":"29_CR26","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1015071400913","volume":"28","author":"E Giunchiglia","year":"2002","unstructured":"Giunchiglia, E., Tacchella, A., Giunchiglia, F.: SAT-based decision procedures for classical modal logics. J. Autom. Reason. 28(2), 143\u2013171 (2002)","journal-title":"J. Autom. Reason."},{"key":"29_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-319-08587-6_31","volume-title":"Automated Reasoning","author":"D Gor\u00edn","year":"2014","unstructured":"Gor\u00edn, D., Pattinson, D., Schr\u00f6der, L., Widmann, F., Wi\u00dfmann, T.: Cool \u2013 a generic reasoner for coalgebraic hybrid logics (system description). In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 396\u2013402. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_31"},{"issue":"3","key":"29_CR28","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1145\/3166.3170","volume":"28","author":"JD Gould","year":"1985","unstructured":"Gould, J.D., Lewis, C.: Designing for usability: key principles and what designers think. Commun. ACM 28(3), 300\u2013311 (1985)","journal-title":"Commun. ACM"},{"key":"29_CR29","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 100\u2013178. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50005-9"},{"issue":"1","key":"29_CR30","first-page":"177","volume":"2","author":"A Heuerding","year":"1996","unstructured":"Heuerding, A., J\u00e4ger, G., Schwendimann, S., Seyfried, M.: The logics workbench LWB: a snapshot. Euromath Bull. 2(1), 177\u2013186 (1996)","journal-title":"Euromath Bull."},{"issue":"2","key":"29_CR31","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1305\/ndjfl\/1093636937","volume":"28","author":"IL Humberstone","year":"1987","unstructured":"Humberstone, I.L.: The modal logic of \u2018all and only\u2019. Notre Dame J. Formal Logic 28(2), 177\u2013188 (1987)","journal-title":"Notre Dame J. Formal Logic"},{"key":"29_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-69778-0_22","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"U Hustadt","year":"1998","unstructured":"Hustadt, U., Schmidt, R.A.: Simplification and backjumping in modal tableau. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 187\u2013201. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-69778-0_22"},{"key":"29_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-38574-2_31","volume-title":"Automated Deduction \u2013 CADE-24","author":"M Kaminski","year":"2013","unstructured":"Kaminski, M., Tebbi, T.: InKreSAT: modal reasoning via incremental reduction to SAT. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 436\u2013442. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_31"},{"issue":"5","key":"29_CR34","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1002\/malq.19870330506","volume":"33","author":"H Kawai","year":"1987","unstructured":"Kawai, H.: Sequential calculus for a first order infinitary temporal logic. Math. Logic Q. 33(5), 423\u2013432 (1987)","journal-title":"Math. Logic Q."},{"key":"29_CR35","unstructured":"Khodadadi, M., Schmidt, R.A., Tishkovsky, D.: MetTeL. http:\/\/www.mettel-prover.org"},{"key":"29_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-40537-2_17","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M Khodadadi","year":"2013","unstructured":"Khodadadi, M., Schmidt, R.A., Tishkovsky, D.: A refined tableau calculus with controlled blocking for the description logic $$\\cal{SHOI}$$ . In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS (LNAI), vol. 8123, pp. 188\u2013202. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40537-2_17"},{"key":"29_CR37","unstructured":"Khodadadi, M., Schmidt, R.A., Tishkovsky, D., Zawidzki, M.: Terminating tableau calculi for modal logic K with global counting operators (2012). http:\/\/www.mettel-prover.org\/papers\/KEn12.pdf"},{"key":"29_CR38","volume-title":"Introduction to Metamathematics","author":"SC Kleene","year":"1950","unstructured":"Kleene, S.C.: Introduction to Metamathematics. Van Nostrand, New York (1950)"},{"key":"29_CR39","unstructured":"Koopmann, P., Schmidt, R.A.: LETHE: saturation-based reasoning for non-standard reasoning tasks. In: Dumontier, M., et al. (eds.) OWL Reasoner Evaluation (ORE-2015), CEUR Workshop Proceedings, vol. 1387, pp. 23\u201330 (2015)"},{"key":"29_CR40","unstructured":"Lagniez, J.M., Le Berre, D., de Lima, T., Montmirail, V.: On checking Kripke models for modal logic K. In: Fontaine, P., Schulz, S., Urban, J. (eds.) Practical Aspects of Automated Reasoning (PAAR 2016), CEUR Workshop Proceedings, vol. 1635, pp. 69\u201381 (2016)"},{"key":"29_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-319-08587-6_6","volume-title":"Automated Reasoning","author":"O Lahav","year":"2014","unstructured":"Lahav, O., Zohar, Y.: SAT-based decision procedure for analytic pure sequent calculi. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 76\u201390. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_6"},{"key":"29_CR42","unstructured":"Le Berre, D., Parrain, A.: The SAT4J library, release 2.2. J. Satisf. Boolean Model. Comput. 7, 59\u201364 (2010)"},{"key":"29_CR43","unstructured":"Lukasiewicz, J., Tarski, A.: Investigations into the sentential calculus. Borkowski 12, 131\u2013152 (1956)"},{"key":"29_CR44","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1016\/j.tcs.2012.12.008","volume":"474","author":"D Miller","year":"2013","unstructured":"Miller, D., Pimentel, E.: A formal framework for specifying sequent calculus proof systems. Theor. Comput. Sci. 474, 98\u2013116 (2013)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR45","unstructured":"Minica, S., Khodadadi, M., Schmidt, R.A., Tishkovsky, D.: Synthesising and implementing tableau calculi for interrogative epistemic logics. In: Fontaine, P., Schmidt, R.A., Schulz, S. (eds.) Practical Aspects of Automated Reasoning (PAAR-2012). EPiC Series in Computing, vol. 21, pp. 109\u2013123. EasyChair (2012)"},{"key":"29_CR46","doi-asserted-by":"crossref","unstructured":"Nielsen, J.: Usability inspection methods. In: Plaisant, C. (ed.) Conference on Human Factors in Computing Systems (CHI 1994), pp. 413\u2013414. ACM (1994)","DOI":"10.1145\/259963.260531"},{"key":"29_CR47","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1093\/logcom\/exu029","volume":"26","author":"V Nigam","year":"2014","unstructured":"Nigam, V., Pimentel, E., Reis, G.: An extended framework for specifying and reasoning about proof systems. J. Logic Comput. 26, 539\u2013576 (2014)","journal-title":"J. Logic Comput."},{"key":"29_CR48","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-08587-6_18","volume-title":"Automated Reasoning","author":"V Nigam","year":"2014","unstructured":"Nigam, V., Reis, G., Lima, L.: Quati: an automated tool for proving permutation lemmas. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 255\u2013261. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_18"},{"issue":"1","key":"29_CR49","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1093\/jigpal\/4.1.109","volume":"4","author":"HJ Ohlbach","year":"1996","unstructured":"Ohlbach, H.J.: Computer support for the development and investigation of logics. Logic J. IGPL 4(1), 109\u2013127 (1996)","journal-title":"Logic J. IGPL"},{"key":"29_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-61511-3_77","volume-title":"Automated Deduction \u2014 Cade-13","author":"HJ Ohlbach","year":"1996","unstructured":"Ohlbach, H.J.: SCAN\u2014elimination of predicate quantifiers. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 161\u2013165. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61511-3_77"},{"key":"29_CR51","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1111\/j.1467-8640.1993.tb00310.x","volume":"9","author":"P Prosser","year":"1993","unstructured":"Prosser, P.: Hybrid algorithms for the constraint satisfaction problem. Comput. Intell. 9, 268\u2013299 (1993)","journal-title":"Comput. Intell."},{"key":"29_CR52","unstructured":"Rothenberg, R.: A class of theorems in \u0141ukasiewicz logic for benchmarking automated theorem provers. In: TABLEAUX, Automated Reasoning with Analytic Tableaux and Related Methods, Position Papers, vol. 7, pp. 101\u2013111 (2007)"},{"key":"29_CR53","unstructured":"Schmidt, R.A., Stell, J.G., Rydeheard, D.: Axiomatic and tableau-based reasoning for Kt(H, R). In: Gor\u00e9, R., Kooi, B., Kurucz, A. (eds.) Advances in Modal Logic, vol. 10, pp. 478\u2013497. College Publications (2014)"},{"issue":"2","key":"29_CR54","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-7(2:6)2011","volume":"7","author":"RA Schmidt","year":"2011","unstructured":"Schmidt, R.A., Tishkovsky, D.: Automated synthesis of tableau calculi. Log. Methods Comput. Sci. 7(2), 1\u201332 (2011)","journal-title":"Log. Methods Comput. Sci."},{"issue":"1","key":"29_CR55","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/2559947","volume":"15","author":"RA Schmidt","year":"2014","unstructured":"Schmidt, R.A., Tishkovsky, D.: Using tableau to decide description logics with full role negation and identity. ACM Trans. Comput. Logic 15(1), 7:1\u20137:31 (2014)","journal-title":"ACM Trans. Comput. Logic"},{"key":"29_CR56","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-24312-2_4","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"RA Schmidt","year":"2015","unstructured":"Schmidt, R.A., Waldmann, U.: Modal tableau systems with blocking and congruence closure. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 38\u201353. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24312-2_4"},{"issue":"13","key":"29_CR57","first-page":"173","volume":"18","author":"AM Sette","year":"1973","unstructured":"Sette, A.M.: On the propositional calculus P1. Math. Japonicae 18(13), 173\u2013180 (1973)","journal-title":"Math. Japonicae"},{"key":"29_CR58","volume-title":"First Order Logic","author":"RM Smullyan","year":"1971","unstructured":"Smullyan, R.M.: First Order Logic. Springer, Berlin (1971)"},{"issue":"4","key":"29_CR59","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1016\/j.jlamp.2015.11.003","volume":"85","author":"JG Stell","year":"2016","unstructured":"Stell, J.G., Schmidt, R.A., Rydeheard, D.E.: A bi-intuitionistic modal logic: foundations and automation. J. Log. Algebraic Methods Program. 85(4), 500\u2013519 (2016)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"29_CR60","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-66902-1_14","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"D Tishkovsky","year":"2017","unstructured":"Tishkovsky, D., Schmidt, R.A.: Rule refinement for semantic tableau calculi. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017. LNCS (LNAI), vol. 10501, pp. 228\u2013244. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66902-1_14"},{"key":"29_CR61","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-22119-4_19","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"D Tishkovsky","year":"2011","unstructured":"Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: $$MetTeL$$ : a tableau prover with logic-independent inference engine. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS (LNAI), vol. 6793, pp. 242\u2013247. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22119-4_19"},{"key":"29_CR62","unstructured":"Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: MetTeL2: towards a tableau prover generation platform. In: Fontaine, P., Schmidt, R.A., Schulz, S. (eds.) Practical Aspects of Automated Reasoning (PAAR-2012). EPiC Series in Computing, vol. 21, pp. 149\u2013162. EasyChair (2012)"},{"key":"29_CR63","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-33353-8_41","volume-title":"Logics in Artificial Intelligence","author":"D Tishkovsky","year":"2012","unstructured":"Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: The tableau prover generator MetTeL2. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds.) JELIA 2012. LNCS (LNAI), vol. 7519, pp. 492\u2013495. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33353-8_41"},{"key":"29_CR64","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-94-010-0387-2_2","volume-title":"Handbook of Philosophical Logic","author":"H Wansing","year":"2002","unstructured":"Wansing, H.: Sequent systems for modal logics. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 8, pp. 61\u2013145. Springer, Dordrecht (2002)"},{"key":"29_CR65","doi-asserted-by":"crossref","unstructured":"Zawidzki, M.: Deductive systems and decidability problem for hybrid logics. Ph.D. thesis, Faculty of Philosophy and History, University of Lodz (2013)","DOI":"10.18778\/7969-042-8"},{"key":"29_CR66","unstructured":"Zhao, Y., Schmidt, R.A.: Forgetting concept and role symbols in $$\\cal{ALCOIH}\\mu ^+(\\nabla ,\\sqcap )$$ -ontologies. In: Kambhampati, S. (ed.) International Joint Conference on Artificial Intelligence (IJCAI 2016), pp. 1345\u20131352. AAAI Press\/IJCAI (2016)"},{"key":"29_CR67","unstructured":"Zohar, Y.: Gen2sat. http:\/\/www.cs.tau.ac.il\/research\/yoni.zohar\/gen2sat.html"},{"key":"29_CR68","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-319-40229-1_33","volume-title":"Automated Reasoning","author":"Y Zohar","year":"2016","unstructured":"Zohar, Y., Zamansky, A.: Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 487\u2013495. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_33"}],"container-title":["Lecture Notes in Computer Science","Description Logic, Theory Combination, and All That"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-22102-7_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,21]],"date-time":"2022-09-21T20:30:38Z","timestamp":1663792238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-22102-7_29"}},"subtitle":["The Case of Two Generic Automated Reasoning Tools"],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030221010","9783030221027"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-22102-7_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"1 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}