Completeness of interpolation algorithms in classical and non-classical logics

DOI10.1016/J.APAL.2026.103808MaRDI QIDQ7304791zbMATH OpenFDO

Authors Stefan Hetzl, Raheleh Jalali, Timo Lang

Publication date 28 July 2026

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.APAL.2026.103808

Mathematics Subject Classification ID

Interpolation, preservation, definability (03C40) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• Abstractions from proofs
• Beth definability in expressive description logics
• Computer Aided Verification
• Constructing Craig interpolation formulas
• Cooperation of background reasoners in theory reasoning by residue sharing
• Handbook of proof theory
• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 3249766 (Why is no real title available?)
• scientific article; zbMATH DE number 3085803 (Why is no real title available?)
• Interpolant strength
• Interpolant strength revisited
• Interpolant-Based Transition Relation Approximation
• Interpolants, cut elimination and flow graphs for the propositional calculus
• Interpolation and model checking
• Interpolation and SAT-based model checking.
• Interpolation and Symbol Elimination
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Introduction: Interpolations -- essays in honor of William Craig
• Lazy Abstraction with Interpolants
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Lower bounds to the size of constant-depth propositional proofs
• Mathematical Logic and Computation
• Methods of cut-elimination
• Nested interpolants
• On formulas of one variable in intuitionistic propositional calculus
• Partition-based logical reasoning for first-order and propositional theories
• Playing in the grey area of proofs
• Proof theory. 2nd ed
• Simplification by Cooperating Decision Procedures
• The intractability of resolution
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Tools and Algorithms for the Construction and Analysis of Systems
• Towards a clausal analysis of cut-elimination

This page was built for publication: Completeness of interpolation algorithms in classical and non-classical logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7304791)