Interpolation, Amalgamation, and Computation

JUNIOR STAR - GACR GM25-18306M [Registered results] 2025 - 2029

Principal Investigator: Ing. Wesley Fussner, Ph.D.

Interpolation is a fundamental metalogical property of broad importance to several fields, including software/hardware verification, databases, mathematics, and philosophy.

This project aims to bridge the gap between the two dominant paradigms in the study of interpolation: the proof-theoretic approach and the algebraic approach. By reconciling these methodologies, the project will develop a systematic account of interpolation in varied environments, and, in particular, will produce a flexible and powerful toolkit for investigating interpolation in different logical contexts.

Our investigation places a special emphasis on finding broadly applicable techniques for understanding computational aspects of interpolation, such as the decidability of various questions relating to interpolation and complexity of the associated algorithms.

Project Aims

  1. Bridge the gap between syntactic and semantic approaches to interpolation.
  2. Provide a systematic account interpolation across different logical contexts.
  3. Deploy insights from the more cohesive framework to deepen our understanding of interpolation in important case studies.