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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Actually, Łukasiewicz called it (the Polish equivalent for) Indeterminate, but to keep things consistent with other works, we use Neither.
- 2.
Named after the authors Jeff and Geoff, for any logic XYZ.
- 3.
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.)
- 4.
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].
- 5.
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.
- 6.
Thanks to Giles Reger for providing a special version of Vampire that normalises the formulae into comparable forms.
References
Avron, A.: Natural 3-valued logics: characterization and proof theory. J. Symb. Log. 56(1), 276–294 (1991)
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_84
Beckert, B., Hähnle, R., Oel, P., Sulzmann, M.: The tableau-based theorem prover
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_95Belnap, 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_2
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)
Evans, G.: Can there be vague objects? Analysis 38, 208 (1978)
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_5
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
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_1
Levine, E., Parks, L.: Undead TV. Duke University Press, Durham (2007)
Łukasiewicz, J.: On three-valued logic. Ruch Filozoficny 5, 170–171 (1920)
Omori, H., Wansing, H.: 40 years of FDE: an introductory overview. Stud. Log. 105(6), 1021–1049 (2017)
Pelletier, F.: Another argument against vague identity. J. Philos. 86, 481–492 (1989)
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)
Priest, G.: The logic of paradox. J. Philos. Log. 8, 219–241 (1979)
Priest, G., Routley, R., Norman, J.: Paraconsistent Logic: Essays on the Inconsistent. Philosophia Verlag (1989)
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/
Sobociński, B.: Axiomatization of a partial system of three-valued calculus of propositions’. J. Comput. Syst. 1, 23–55 (1952)
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)
Wikipedia contributors: logic - Wikipedia, the free encyclopedia (2018). https://en.wikipedia.org/w/index.php?title=Logic&oldid=875884116
version 4.0. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 303–307. Springer, Heidelberg (1996). Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Sutcliffe, G., Pelletier, F.J. (2019). JGXYZ: An ATP System for Gap and Glut Logics. In: Fontaine, P. (eds) Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science(), vol 11716. Springer, Cham. https://doi.org/10.1007/978-3-030-29436-6_31
Download citation
DOI: https://doi.org/10.1007/978-3-030-29436-6_31
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-29435-9
Online ISBN: 978-3-030-29436-6
eBook Packages: Computer ScienceComputer Science (R0)