Complexity of Craig’s Interpolation

Article type: Research Article

Authors: Mundici, Daniele

Affiliations: Nacional Researche Council, Florence

Abstract: In this paper we investigate the length ‖χ‖ of the shortest interpolant of a valid implication φ→ψ in terms of ‖φ‖+‖ψ‖, both in sentential and in first-order logic. In the case of sentential logic, we give a precise exponential upper bound for ‖χ‖. We also show that the information about the growth of ‖χ‖ has some implications for computation theory. In the case of first-order logic we exhibit a very short valid implication whose interpolants are all impossibly long.

Keywords: Valid implication, logical circuit, interpolant, delay complexity

DOI: 10.3233/FI-1982-53-403

Journal: Fundamenta Informaticae, vol. 5, no. 3-4, pp. 261-278, 1982