×

zbMATH — the first resource for mathematics

Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi. (English) Zbl 06623281
Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-40228-4/pbk; 978-3-319-40229-1/ebook). Lecture Notes in Computer Science 9706. Lecture Notes in Artificial Intelligence, 487-495 (2016).
Summary: Gen2sat [1] is an efficient and generic tool that can decide derivability for a wide variety of propositional non-classical logics given in terms of a sequent calculus. It contributes to the line of research on computer-supported tools for investigation of logics in the spirit of the “logic engineering” paradigm. Its generality and efficiency are made possible by a reduction of derivability in analytic pure sequent calculi to SAT. This also makes Gen2sat a “plug-and-play” tool so it is compatible with any standard off-the-shelf SAT solver and does not require any additional logic-specific resources. We describe the implementation details of Gen2sat and an evaluation of its performance, as well as a pilot study for using it in a “hands on” assignment for teaching the concept of sequent calculi in a logic class for engineering practitioners.
For the entire collection see [Zbl 1337.68016].

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Gen2sat website. http://www.cs.tau.ac.il/research/yoni.zohar/gen2sat
[2] Areces, C.E.: Logic engineering: the case of description and hybrid logics. Institute for Logic, Language and Computation (2000)
[3] Avron, A.: Gentzen-type systems, resolution, tableaux. J. Autom. Reasoning 10(2), 265–281 (1993) · Zbl 0788.03013 · doi:10.1007/BF00881838
[4] Avron, A., Konikowska, B., Zamansky, A.: Efficient reasoning with inconsistent information using C-systems. Inf. Sci. 296, 219–236 (2015) · Zbl 1360.68827 · doi:10.1016/j.ins.2014.11.003
[5] Baaz, M., Fermüller, 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–230. Springer, Heidelberg (1996) · doi:10.1007/3-540-61511-3_84
[6] Carnielli, W., Coniglio, M.E., Marcos, J.: Logics of formal inconsistency. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 14, pp. 1–93. Springer, New York (2007) · Zbl 1266.03006 · doi:10.1007/978-1-4020-6324-4_1
[7] 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–133. Springer, Heidelberg (2013) · Zbl 1432.68546 · doi:10.1007/978-3-642-35722-0_9
[8] Ciabattoni, A., Spendier, L.: Tools for the investigation of substructural and paraconsistent logics. In: Fermé, E., Leite, J. (eds.) JELIA 2014. LNCS, vol. 8761, pp. 18–32. Springer, Heidelberg (2014) · Zbl 1432.68547 · doi:10.1007/978-3-319-11558-0_2
[9] Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive OR. In: 2003 Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, pp. 271–280, June 2003 · doi:10.1109/LICS.2003.1210067
[10] Cotrini, C., Gurevich, Y.: Basic primal infon logic. J. Logic Comput. 26(1), 117–141 (2013) · Zbl 1403.03050 · doi:10.1093/logcom/ext021
[11] da Costa, N.C.: Sistemas formais inconsistentes, vol. 3. Editora UFPR (1993) · Zbl 0798.03025
[12] Degtyarev, A., Voronkov, A.: The inverse method. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 179–272. MIT Press, Cambridge (2001) · Zbl 0992.03016 · doi:10.1016/B978-044450813-3/50006-0
[13] 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–322. Springer, Heidelberg (2005) · Zbl 1142.68497 · doi:10.1007/11554554_25
[14] Hoffmann, M., Iachelini, G.: Code coverage analysis for eclipse. In: Eclipse Summit Europe (2007)
[15] Kawai, H.: Sequential calculus for a first order infinitary temporal logic. Math. Logic Q. 33(5), 423–432 (1987) · Zbl 0611.03010 · doi:10.1002/malq.19870330506
[16] Lahav, O., Zohar, Y.: SAT-based decision procedure for analytic pure sequent calculi. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 76–90. Springer, Heidelberg (2014) · Zbl 1433.03025 · doi:10.1007/978-3-319-08587-6_6
[17] Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. J. Satisfiability Boolean Mode. Comput. 7, 59–64 (2010)
[18] Neto, A., Finger, M.: Effective prover for minimal inconsistency logic. In: Bramer, M. (ed.) Artificial Intelligence in Theory and Practice. IFIP, vol. 217, pp. 465–474. Springer US, London (2006) · doi:10.1007/978-0-387-34747-9_48
[19] Neto, A., Finger, M.: Kems-a multi-strategy tableau prover. In: Proceedings of the VI Best MSc Dissertation/PhD Thesis Contest (CTDIA 2008), Salvador (2008)
[20] Neto, A., Kaestner, C.A.A., Finger, M.: Towards an efficient prover for the paraconsistent logic C1. Electron. Notes Theoret. Comput. Sci. 256, 87–102 (2009) · Zbl 1291.03020 · doi:10.1016/j.entcs.2009.11.007
[21] Ohlbach, H.J.: Computer support for the development and investigation of logics. Logic J. IGPL 4(1), 109–127 (1996) · Zbl 0859.68094 · doi:10.1093/jigpal/4.1.109
[22] Olivetti, N., Pozzato, G.L.: NESCOND: an implementation of nested sequent calculi for conditional logics. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 511–518. Springer, Heidelberg (2014) · Zbl 1425.68378 · doi:10.1007/978-3-319-08587-6_39
[23] Page, R.L.: Software is discrete mathematics. ACM SIGPLAN Not. 38, 79–86 (2003). ACM · doi:10.1145/944746.944713
[24] Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: Mettel2: towards a tableau prover generation platform. In: PAAR@ IJCAR, pp. 149–162 (2012)
[25] Zamansky, A., Farchi, E.: Teaching logic to information systems students: challenges and opportunities. In: Fourth International Conference on Tools for Teaching Logic, TTL (2015)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.