nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

JGXYZ: An ATP System for Gap and Glut Logics

verfasst von : Geoff Sutcliffe, Francis Jeffry Pelletier

Erschienen in: Automated Deduction – CADE 27

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

This paper describes an ATP system, named JGXYZ, for some gap and glut logics. JGXYZ is based on an equi-provable translation to FOL, followed by use of an existing ATP system for FOL. A key feature of JGXYZ is that the translation to FOL is data-driven, in the sense that it requires only the addition of a new logic’s truth tables for the unary and binary connectives in order to produce an ATP system for the logic. Experimental results from JGXYZ illustrate the differences between the logics and translated problems, both technically and in terms of a quasi-real-world use case.

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 Certified Equational Reasoning via Ordered Completion

Nächstes Kapitel GKC: A Reasoning System for Large Knowledge Bases

Actually, Łukasiewicz called it (the Polish equivalent for) Indeterminate, but to keep things consistent with other works, we use Neither.

Named after the authors Jeff and Geoff, for any logic XYZ.

Computer geeks ... think of the characters as UNIX processes, which can be alive, not alive, or zombies. Burial corresponds to reaping the process from the process table. FDE can thus be used to reason about UNIX processes. (Thanks to Josef Urban for this interpretation.)

The classical interpretation of equality is due to the classical interpretation of terms. Since a term is interpreted as an element of the domain, if two terms are interpreted as the same element then their equality is True, and if they are interpreted as different elements then their equality is False. There is no middle ground (Both or Neither). [7, 14].

This can be used to empirically check that the translation does produce equi-provable problems. For more fun, it is possible to repeatedly apply the translation to a FOL problem to produce a new FOL problem, to produce a sequence of ever more difficult FOL problems.

Thanks to Giles Reger for providing a special version of Vampire that normalises the formulae into comparable forms.

Avron, A.: Natural 3-valued logics: characterization and proof theory. J. Symb. Log. 56(1), 276–294 (1991)MathSciNetCrossRef

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). https://doi.org/10.1007/3-540-61511-3_84CrossRef

Beckert, B., Hähnle, R., Oel, P., Sulzmann, M.: The tableau-based theorem prover

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-29436-6_31/MediaObjects/478046_1_En_31_Fige_HTML.gif

version 4.0. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 303–307. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61511-3_95

Belnap, N.D.: A Useful Four-Valued Logic. In: Dunn, J.M., Epstein, G. (eds.) Modern Uses of Multiple-Valued Logic. EPIS, vol. 2, pp. 5–37. Springer, Dordrecht (1977). https://doi.org/10.1007/978-94-010-1161-7_2CrossRef

Belnap, N.: A useful four-valued logic: how a computer should think. In: Anderson, A., Belnap, N., Dunn, J. (eds.) Entailment: The Logic of Relevance and Necessity, vol. 2, pp. 506–541. Princeton University Press (1992)

Dunn, J.: Intuitive semantics for first degree entailment and coupled trees. Philos. Stud. 29, 149–168 (1976)MathSciNetCrossRef

Evans, G.: Can there be vague objects? Analysis 38, 208 (1978)CrossRef

Hähnle, R.: Advanced Many-Valued Logics. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic. HALO, vol. 2, pp. 297–395. Springer, Dordrecht (2001). https://doi.org/10.1007/978-94-017-0452-6_5CrossRef

Hazen, A., Pelletier, F.: K3, Ł3, LP, RM3, A3, FDE, M: How to Make Many-Valued Logics Work for You. In: Omori, H., Wansing, H. (eds.) New Essays on Belnap-Dunn Logic. Springer, Berlin (1980). To appear. Synthese Library

10.

Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1CrossRef

11.

Levine, E., Parks, L.: Undead TV. Duke University Press, Durham (2007)CrossRef

12.

Łukasiewicz, J.: On three-valued logic. Ruch Filozoficny 5, 170–171 (1920)

13.

Omori, H., Wansing, H.: 40 years of FDE: an introductory overview. Stud. Log. 105(6), 1021–1049 (2017)MathSciNetCrossRef

14.

Pelletier, F.: Another argument against vague identity. J. Philos. 86, 481–492 (1989)MathSciNetCrossRef

15.

Pelletier, F., Sutcliffe, G., Hazen, A.: Automated reasoning for the dialetheic logic RM3. In: Rus, V., Markov, Z. (eds.) Proceedings of the 30th International FLAIRS Conference, pp. 110–115 (2017)

16.

Priest, G.: The logic of paradox. J. Philos. Log. 8, 219–241 (1979)MathSciNetCrossRef

17.

Priest, G., Routley, R., Norman, J.: Paraconsistent Logic: Essays on the Inconsistent. Philosophia Verlag (1989)

18.

Shapiro, S., Kouri Kissel, T.: Classical logic. In: Zalta, E. (ed.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University (2018). https://plato.stanford.edu/archives/spr2018/entries/logic-classical/

19.

Sobociński, B.: Axiomatization of a partial system of three-valued calculus of propositions’. J. Comput. Syst. 1, 23–55 (1952)MathSciNetMATH

20.

Sutcliffe, G., Pelletier, F., Hazen, A.: Making Belnap’s “useful four-valued logic” useful. In: Brawner, K., Rus, V. (eds.) Proceedings of the 31st International FLAIRS Conference, pp. 116–121 (2018)

21.

Wikipedia contributors: logic - Wikipedia, the free encyclopedia (2018). https://en.wikipedia.org/w/index.php?title=Logic&oldid=875884116

Titel: JGXYZ: An ATP System for Gap and Glut Logics
verfasst von: Geoff Sutcliffe
Francis Jeffry Pelletier
Verlag: Springer International Publishing
Buch: Automated Deduction – CADE 27
Print ISBN: 978-3-030-29435-9

Electronic ISBN: 978-3-030-29436-6

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-29436-6_31

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner