User Settings
Open AccessArticle10.29007/xt3j

Instantiations, Zippers and EPR Interpolation

Nikolaj Bjørner,Arie Gurfinkel,Konstantin Korovin,Ori Lahav-2018-01-23-EPiC series in computing
5PDF

TL;DRAbstract

This paper describes interpolation procedures for EPR. In principle, interpolation for EPR is simple: It is a special case of first-order interpolation. In practice, we would like procedures that take advantage of properties of EPR: EPR admits finite models and those models are sometimes possible to describe very compactly. Inspired by procedures for propositional logic that use models and cores, but not proofs, we develop a procedure for EPR that uses just models and cores.

Chat with Paper

AI Agents for this Paper

This paper describes interpolation procedures for EPR. In principle, interpolation for EPR is simple: It is a special case of first-order interpolation. In practice, we would like procedures that take advantage of properties of EPR: EPR admits finite models and those models are sometimes possible to describe very compactly. Inspired by procedures for propositional logic that use models and cores, but not proofs, we develop a procedure for EPR that uses just models and cores.

Keywords

Interpolation (computer graphics)Electron paramagnetic resonanceMathematical proofComputer scienceMathematicsAlgorithmAlgebra over a fieldPure mathematics

Chat

Click to start Chat