Tautology Elimination, Cut Elimination, and S5
DOI: http://dx.doi.org/10.12775/LLP.2017.005
Abstract
Keywords
Full Text:
PDFReferences
Brighton, J., “Cut elimination for GLS using the terminability of its regress process”, Journal of Philosophical Logic 5, 2 (2016): 147–153. DOI: 10.1007/s10992-015-9368-4
Bednarska, K., and A. Indrzejczak, “Hypersequent calculi for S5: The methods of cut elimination”, Logic and Logical Philosophy 24, 3 (2015): 277–311. DOI: 10.12775/LLP.2015.018
Davis, M., and H. Putnam, “A computing procedure for quantification theory”, Journal of the Assoc. Comput. Mach. 7, 3 (1960): 201–215. DOI: 10.1145/321033.321034
Fitting, M., Proof Methods for Modal and Intuitionistic Logics, Reidel, Dordrecht 1983. DOI: 10.1007/978-94-017-2794-5
Fitting, M., “Simple propositional S5 tableau system”, Annals of Pure and Applied Logic 96, 1–3 (1999): 101–115. DOI: 10.1016/S0168-0072(98)00034-7
Gallier, J.H., Logic for Computer Science, Harper and Row, New York 1986.
Gao, F., and G. Tourlakis, “A short and readable proof of cut elimination for two first-order modal logics”, Bulletin of the Section of Logic 44, 3–4 (2015): 131–148. DOI: 10.18778/0138-0680.44.3.4.03
Indrzejczak, A., “Simple decision procedure for S5 in standard cut-free sequent calculus”, Bulletin of the Section of Logic 45, 2 (2016): 125–140. DOI: 10.18778/0138-0680.45.2.05
Lyaletski, A.V., “A note on the cut rule”, in Abstracts of the International Conference “Maltsev Meeting”, vol. 137, Novosibirsk 2011.
Negri, S., and J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge 2001. DOI: 10.1017/CBO9780511527340
Ohnishi, M., K. Matsumoto, “Gentzen method in modal calculi I”, Osaka Mathematical Journal 9 (1957): 113–130.
Print ISSN: 1425-3305
Online ISSN: 2300-9802