## Unification and admissible rules for paraconsistent minimal Johanssons’ logic J and positive intuitionistic logic $$\mathbf{IPC}^+$$.(English)Zbl 1323.03029

Summary: We study unification problem and problem of admissibility for inference rules in minimal Johanssons’ logic J and positive intuitionistic logic $$\mathrm{IPC}^+$$. This paper proves that the problem of admissibility for inference rules with coefficients (parameters) (as well as plain ones – without parameters) is decidable for the paraconsistent minimal Johanssons’ logic J and the positive intuitionistic logic $$\mathrm{IPC}^+$$. Using obtained technique we show also that the unification problem for these logics is also decidable: we offer algorithms which compute complete sets of unifiers for any unifiable formula. Checking just unifiability of formulas with coefficients also works via verification of admissibility.

### MSC:

 03B53 Paraconsistent logics 03B25 Decidability of theories and sets of sentences 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text:

### References:

 [1] Baader, F.; Ghilardi, S., Unification in modal and description logics, Log. J. IGPL, 19, 6, 705-730, (2011) · Zbl 1258.03018 [2] F. Baader, R. Küsters, Unification in a description logic with transitive closure of roles, in: LPAR, 2001, pp. 217-232. · Zbl 1275.68134 [3] Baader, F.; Morawska, B., Unification in the description logic EL, Log. Methods Comput. Sci., 6, 3, 1-31, (2010) · Zbl 1214.68379 [4] Baader, F.; Narendran, P., Unification of concept terms in description logics, J. Symbolic Comput., 31, 3, 277-305, (2001) · Zbl 0970.68166 [5] Baader, F.; Snyder, W., Unification theory, (Robinson, J. A.; Voronkov, A., Handbook of Automated Reasoning, vol. I, (2001), Elsevier Science Publishers), 447-533 · Zbl 1011.68126 [6] Babenyshev, S.; Rybakov, V., Linear temporal logic LTL: basis for admissible rules, J. Logic Comput., 21, 2, 157-177, (2011) · Zbl 1233.03026 [7] Babenyshev, S.; Rybakov, V., Unification in linear temporal logic LTL, Ann. Pure Appl. Logic, 162, 12, 991-1000, (2011) · Zbl 1241.03014 [8] Friedman, H., One hundred and two problems in mathematical logic, J. Symbolic Logic, 40, 3, 113-130, (1975) · Zbl 0318.02002 [9] Ghilardi, S., Unification through projectivity, J. Logic Comput., 7, 6, 733-752, (1997) · Zbl 0894.08004 [10] Ghilardi, S., Unification in intuitionistic logic, J. Symbolic Logic, 64, 2, 859-880, (1999) · Zbl 0930.03009 [11] Ghilardi, S., Best solving modal equations, Ann. Pure Appl. Logic, 102, 3, 183-198, (2000) · Zbl 0949.03010 [12] Iemhoff, R., On the admissible rules of intuitionistic propositional logic, J. Symbolic Logic, 66, 1, 281-294, (2001) · Zbl 0986.03013 [13] R. Iemhoff, Towards a proof system for admissibility, in: CSL 2003, 2003, pp. 255-270. · Zbl 1116.03304 [14] Iemhoff, R.; Metcalfe, G., Proof theory for admissible rules, Ann. Pure Appl. Logic, 159, 1-2, 171-186, (2009) · Zbl 1174.03024 [15] Jerabek, E., Admissible rules of modal logics, J. Logic Comput., 15, 4, 411-431, (2005) · Zbl 1077.03011 [16] Jerabek, E., Complexity of admissible rules, Arch. Math. Logic, 46, 2, 73-92, (2007) · Zbl 1115.03010 [17] Jerabek, E., Independent bases of admissible rules, Log. J. IGPL, 16, 3, 249-267, (2008) · Zbl 1146.03008 [18] Jerabek, E., Bases of admissible rules of lukasiewicz logic, J. Logic Comput., 20, 6, 1149-1163, (2010) · Zbl 1216.03043 [19] Jerabek, E., Admissible rules of lukasiewicz logic, J. Logic Comput., 20, 2, 425-447, (2010) · Zbl 1216.03042 [20] Johansson, I., Der minimalkalkül, ein reduzierter intuitionistischer formalismus, Compos. Math., 4, 119-136, (1937) · JFM 62.1045.08 [21] Kolmogorov, A. N., On the principle of excluded middle, Mat. Sb., 32, 4, 646-667, (1925), (in Russian). English translation [37], 414-437 [22] Maksimova, L. L., A method of proving interpolation in paraconsistent extensions of the minimal logic, Algebra and Logic, 46, 7, 341-353, (2007) · Zbl 1164.03312 [23] Maksimova, L. L., Decidability of the interpolation problem and of related properties in tabular logics, Algebra and Logic, 48, 6, 426-448, (2009) · Zbl 1241.03032 [24] Maksimova, L. L., Decidability of the weak interpolation property over the minimal logic, Algebra and Logic, 50, 2, 106-132, (2011) · Zbl 1285.03029 [25] Odintsov, S. P., Constructive negations and paraconsistency, (2008), Springer Dordrecht · Zbl 1161.03014 [26] Priest, G., Paraconsistent logic. Stanford encyclopedia of philosophy [27] Rautenberg, W., Klassische und nicht-klassische aussagenlogik, (1979), Vieweg Braunschweig · Zbl 0424.03007 [28] Rybakov, V., A criterion for admissibility of rules in the modal system S4 and the intuitionistic logic, Algebra and Logic, 23, 5, 369-384, (1984) · Zbl 0598.03013 [29] Rybakov, V. V., Problems of substitution and admissibility in the modal system grz and in intuitionistic propositional calculus, Ann. Pure Appl. Logic, 50, 1, 71-106, (1990) · Zbl 0709.03009 [30] Rybakov, V. V., Rules of inference with parameters for intuitionistic logic, J. Symbolic Logic, 57, 3, 912-923, (1992) · Zbl 0788.03007 [31] Rybakov, V. V., Construction of an explicit basis for rules admissible in modal system S4, Math. Log. Q., 47, 4, 441-446, (2001) · Zbl 0992.03027 [32] Rybakov, V. V., Logics with the universal modality and admissible consecutions, J. Appl. Non-Classical Logics, 17, 3, 383-396, (2007) · Zbl 1186.03048 [33] Rybakov, V. V., Linear temporal logic with until and next, logical consecutions, Ann. Pure Appl. Logic, 155, 1, 32-45, (2008) · Zbl 1147.03008 [34] Rybakov, V. V., Multi-modal and temporal logics with universal formula - reduction of admissibility to validity and unification, J. Logic Comput., 18, 4, 509-519, (2008) · Zbl 1149.03017 [35] Rybakov, V. V., Rules admissible in transitive temporal logic TS4, sufficient condition, Theoret. Comput. Sci., 411, 50, 4323-4332, (2010) · Zbl 1209.03011 [36] Segerberg, K., Propositional logics related to heytingʼs and johanssonʼs, Theoria, 34, 1, 26-61, (1968) [37] van Heijenoort, J., From frege to Gödel. A sourse book in mathematical logic, (1967), Harvard University Press Cambridge, pp. 1879-1931
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.