Preservation of Craig interpolation by the product of matrix logics. (English) Zbl 1284.03214
Summary: The product of matrix logics, possibly with additional interaction axioms, is shown to preserve a slightly relaxed notion of Craig interpolation. The result is established symbolically, capitalizing on the complete axiomatization of the product of matrix logics provided by their meet-combination. Along the way preservation of the metatheorem of deduction is also proved. The computation of the interpolant in the resulting logic is proved to be polynomially reducible to the computation of the interpolants in the two given logics. Illustrations are provided for classical, intuitionistic and modal propositional logics.
Software:
FOCIReferences:
| [1] | Areces, C.; Hoogland, E.; de Jongh, D., Interpolation, definability and fixed points in interpretability logics, (Advances in Modal Logic. Advances in Modal Logic, CSLI Lecture Notes, vol. 119 (2001), CSLI Publications), 35-58 · Zbl 1001.03054 |
| [2] | Bicarregui, J.; Dimitrakos, T.; Gabbay, D.; Maibaum, T., Interpolation in practical formal development, Logic Journal of the IGPL, 9, 2, 231-243 (2001) · Zbl 0981.03035 |
| [3] | Carbone, A., The Craig interpolation theorem for schematic systems, (Collegium Logicum, vol. 2. Collegium Logicum, vol. 2, Colloquium Logicum Ann. Kurt-Gödel-Society, vol. 2 (1996), Springer), 87-100 · Zbl 0855.03031 |
| [4] | Carnielli, W. A.; Rasga, J.; Sernadas, C., Preservation of interpolation features by fibring, Journal of Logic and Computation, 18, 1, 123-151 (2008) · Zbl 1138.03010 |
| [5] | Craig, W., Linear reasoning. A new form of the Herbrand-Gentzen theorem, The Journal of Symbolic Logic, 22, 250-268 (1957) · Zbl 0081.24402 |
| [6] | Czelakowski, J.; Pigozzi, D., Amalgamation and interpolation in abstract algebraic logic, (Models, Algebras, and Proofs. Models, Algebras, and Proofs, Lecture Notes in Pure and Applied Mathematics, vol. 203 (1999), Dekker), 187-265 · Zbl 0927.03086 |
| [7] | Fitting, M., Proof Methods for Modal and Intuitionistic Logics, Synthese Library, vol. 169 (1983), D. Reidel Publishing Co. · Zbl 0523.03013 |
| [8] | Font, J. M.; Jansana, R.; Pigozzi, D., Fully adequate Gentzen systems and the deduction theorem, Reports on Mathematical Logic, 35, 115-165 (2001) · Zbl 1004.03053 |
| [9] | Gabbay, D. M., Craigʼs interpolation theorem for modal logics, (Conference in Mathematical Logic. Conference in Mathematical Logic, Lecture Notes in Mathematics, vol. 255 (1972), Springer), 111-127 · Zbl 0233.02009 |
| [10] | Gabbay, D. M.; Maksimova, L., Interpolation and Definability: Modal and Intuitionistic Logics, Oxford Logic Guides, vol. 46 (2005), The Clarendon Press, Oxford University Press · Zbl 1091.03001 |
| [11] | Gabbay, D.; Schlechta, K., Conditionals and Modularity in General Logics (2011), Springer · Zbl 1234.03001 |
| [12] | Jhala, R.; McMillan, K. L., Interpolant-based transition relation approximation, Logical Methods in Computer Science, 3(4):4:1 (2007), 17 pp. (electronic) · Zbl 1131.68062 |
| [13] | Kracht, M.; Wolter, F., Properties of independently axiomatizable bimodal logics, The Journal of Symbolic Logic, 56, 4, 1469-1485 (1991) · Zbl 0743.03013 |
| [14] | Maehara, S., On the interpolation theorem of Craig, Mathematical Society of Japan. Sugaku (Mathematics), 12, 235-237 (1960/1961) · Zbl 0123.24601 |
| [15] | Marx, M.; Areces, C., Failure of interpolation in combined modal logics, Notre Dame Journal of Formal Logic, 39, 2, 253-273 (1998) · Zbl 0968.03025 |
| [16] | McMillan, K. L., An interpolating theorem prover, Theoretical Computer Science, 345, 1, 101-121 (2005) · Zbl 1079.68092 |
| [17] | Miller, C.; Kupferschmid, S.; Lewis, M.; Becker, B., Encoding techniques, Craig interpolants and bounded model checking for incomplete designs, (Theory and Applications of Satisfiability Testing—SAT. Theory and Applications of Satisfiability Testing—SAT, Lecture Notes in Computer Science, vol. 6175 (2010), Springer), 194-208 · Zbl 1306.68168 |
| [18] | Mundici, D., NP and Craigʼs interpolation theorem, (Logic Colloquiumʼ82, vol. 112 (1984), North-Holland), 345-358 · Zbl 0594.03021 |
| [19] | Schumm, G. F., Some failures of interpolation in modal logic, Notre Dame Journal of Formal Logic, 27, 1, 108-110 (1986) · Zbl 0588.03009 |
| [20] | Sernadas, A.; Sernadas, C.; Rasga, J., On meet-combination of logics, Journal of Logic and Computation, 22, 6, 1453-1470 (2012) · Zbl 1280.03034 |
| [21] | Urquhart, A., Failure of interpolation in relevant logics, Journal of Philosophical Logic, 22, 5, 449-479 (1993) · Zbl 0798.03020 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
