Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
A Logical Framework for Developing and Mechanizing Set Theories Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi

verfasst von : Yoni Zohar, Anna Zamansky

Erschienen in: Automated Reasoning

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Intuitionistic Layered Graph Logic
Nächstes Kapitel Model Checking Parameterised Multi-token Systems via the Composition Method
Fußnoten
1
We take sequents to be pairs of sets of formulas, and therefore exchange and contraction are built in.
 
2
Paralyzer is a tool that transforms Hilbert calculi of a certain general form into equivalent analytic sequent calculi. It was described in [7] and can be found at http://​www.​logic.​at/​people/​lara/​paralyzer.​html.
 
3
The tableau calculus for \(C_1\) in \({\text {KEMS}}\) can be translated to a sequent calculus (the connection between the two frameworks was discussed e.g. in [3]). However, the translated sequent calculus is non-analytic,and thus cannot be used with Gen2sat.
 
4
Out of 11 possible formula comparator choices of KEMS, Table 1 presents the results for the best performing one in each problem.
 
5
The second author has been teaching the course for several years at the University of Haifa; see [25] for further details on the course design.
 
6
Interestingly, seven students employed new connectives with arity greater than 2 and three employed also 0-ary connectives (which indeed increased coverage), although they have not seen any such example in class.
 
Literatur
1.
2.
Areces, C.E.: Logic engineering: the case of description and hybrid logics. Institute for Logic, Language and Computation (2000)
3.
4.
Avron, A., Konikowska, B., Zamansky, A.: Efficient reasoning with inconsistent information using C-systems. Inf. Sci. 296, 219–236 (2015)MathSciNetCrossRef
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)CrossRef
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)CrossRef
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)CrossRef
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)
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
10.
Cotrini, C., Gurevich, Y.: Basic primal infon logic. J. Logic Comput. 26(1), 117–141 (2013)MATH
11.
da Costa, N.C.: Sistemas formais inconsistentes, vol. 3. Editora UFPR (1993)
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)CrossRef
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)CrossRef
14.
Hoffmann, M., Iachelini, G.: Code coverage analysis for eclipse. In: Eclipse Summit Europe (2007)
15.
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)
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)CrossRef
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)MathSciNetCrossRefMATH
21.
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)
23.
Page, R.L.: Software is discrete mathematics. ACM SIGPLAN Not. 38, 79–86 (2003). ACMCrossRef
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)
Metadaten
Titel
Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi
verfasst von
Yoni Zohar
Anna Zamansky
Copyright-Jahr
2016
Buch
Automated Reasoning

Print ISBN: 978-3-319-40228-4

Electronic ISBN: 978-3-319-40229-1

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-40229-1_33