A simple algebraic proof of the equational interpolation theorem
In this paper, the author gives a proof of the following interpolation theorem for equational logic: Let \(X\) and \(Y\) be sets of equations such that \(X\models Y\). Then there exists a set \(I\) of interpolant equations, with all its non-logical symbols both in \(X\) and \(Y\), such that \(X\models I\) and \(I\models Y\). The result is obtained through a simple algebraic construction. Many- sorted algebras are involved and the necessary extension of the notion of a signature is made, but the result can also be taken within traditional equational logic.
- A semantic approach to interpolation
- Interpolation in computing science: The semantics of modularization
- Interpolation in Grothendieck institutions
- Category-based modularisation for equational logic programming
- Generalised graded interpolation
- The institution-theoretic scope of logic theorems
- Interpolation for predefined types
- Abstract Beth definability in institutions
- scientific article; zbMATH DE number 23769 (Why is no real title available?)
- An axiomatic approach to structuring specifications
- Craig interpolation for networks of sentences
- scientific article; zbMATH DE number 1543346 (Why is no real title available?)
- Interpolation and compactness in categories of pre-institutions
- Three interpolation theorems for typeless logics
- An introduction to category-based equational logic
- Property-oriented semantics of structured specifications
- Equational axiomatizability for coalgebra
- Proving interpolation for conditional equational logic, using functions to represent conditionals
- On the fragility of interpolation
- An institution-independent proof of the Robinson consistency theorem
This page was built for publication: A simple algebraic proof of the equational interpolation theorem
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1173754)