Mathematical Text Processing in EA-style: a Sequent Aspect

Journal of Formalized Reasoning

Alexander Lyaletski

关键词: Evidence Algorithm;    sequent calculus;    classical logic;    intuitionistic logic;    modal logic;   

DOI  :  10.6092/issn.1972-5787/4569

学科分类：计算机科学（综合）

来源: Universita degli Studi di Bologna

【 摘 要 】

The paper is devoted to the study of one of the aspects ofthe so-called Evidence Algorithm programme advanced byAcademician V.M.~Glushkov and connected with the problem ofautomated theorem-proving search in the signature of first-order theoriesthat can use different logics, such as classical, intuitionistic, andmodal ones.An approach to the construction of such sequent logics (with or without equality)is described.It exploits the originalnotions of admissibility and compatibility, which permits to avoid preliminary skolemization being a forbiddenoperation for a number of non-classical logics in general. Following the approach, the cut-free sequent (modal)calculi avoiding the dependence of inference search on different orders of quantifier rules applications are described.Results on the coextensivity of sequent calculi are given. The research gives a way to theconstruction of computer-oriented quantifier-rule-free calculi for classical and intuitionistic logics and their modal extensions.

【 授权许可】

CC BY