|Title:||Interpolation in first-order logic with equality||Other Titles:||Interpolation in der Prädikatenlogik mit Gleichheit||Language:||English||Authors:||Mallinger, Bernhard||Qualification level:||Diploma||Advisor:||Hetzl, Stefan||Issue Date:||2014||Number of Pages:||87||Qualification level:||Diploma||Abstract:||
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
|Library ID:||AC12110884||Organisation:||E104 - Institut für Diskrete Mathematik und Geometrie||Publication Type:||Thesis
|Appears in Collections:||Thesis|
Show full item record
Files in this item:
|Mallinger Bernhard - 2014 - Interpolation in first-order logic with equality.pdf||848.05 kB||Adobe PDF|
checked on Jun 19, 2021
checked on Jun 19, 2021
Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.