Title: Interpolation in first-order logic with equality
Other Titles: Interpolation in der Prädikatenlogik mit Gleichheit
Language: input.forms.value-pairs.iso-languages.en
Authors: Mallinger, Bernhard 
Qualification level: Diploma
Advisor: Hetzl, Stefan 
Issue Date: 2014
Mallinger, B. (2014). Interpolation in first-order logic with equality [Diploma Thesis]. reposiTUm. https://doi.org/10.34726/hss.2014.24329
Number of Pages: 87
Qualification level: Diploma
Craig's interpolation theorem is a long known basic result of mathematical logic. Interpolants lay bare certain logical relations between formulas or sets of formulas in a concise way and can often be calculated efficiently from proofs of these relations. Leveraging the tremendous progress of automatic deduction systems in the last decades, obtaining the required proofs is feasible. This enables real world applications for instance in the area of software verification. For practical applicability, interpolation is often studied in relatively weak formalisms such as propositional logic. This thesis however aims at giving a comprehensive account of existing techniques and results with respect to unrestricted classical first-order logic with equality. It is structured into three parts: First, we present Craig's initial proof of the interpolation theorem by reduction to first-order logic without equality and function symbols. Due to the inherent overhead, this approach only gives rise to an impractical algorithm for interpolant extraction. Second, a constructive proof by Huang is introduced in slightly improved form. It employs direct interpolant extraction from resolution proofs in two phases and thereby shows that even in full first-order logic with equality, interpolants can efficiently be calculated. Moreover, we present an analysis of the number of quantifier alternations of the interpolants produced by this algorithm. We additionally propose a novel approach which combines the two phases of Huang's algorithm and thereby allows for creating non-prenex interpolants. Third, we give a semantic perspective on interpolation in the form of a model-theoretic proof based on Robinson's joint consistency theorem. This illustrates the similarities and differences between the proof-theoretic and the model-theoretic view on interpolation.
Keywords: Craig Interpolation; Prädikatenlogik; Interpolantenextraktion
Craig Interpolation; First-Order Logic; Interpolant Extraction
URI: https://doi.org/10.34726/hss.2014.24329
DOI: 10.34726/hss.2014.24329
Library ID: AC12110884
Organisation: E104 - Institut für Diskrete Mathematik und Geometrie 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.

Page view(s)

checked on Jul 2, 2022


checked on Jul 2, 2022

Google ScholarTM