Rebola Pardo, A. (2022). Interpolants and Interference. In M. Benedikt, P. Rümmer, & C. Wernhard (Eds.), iPRA 2022 : The 4th Workshop on Interpolation: From Proofs to Applications : Book of Abstracts (pp. 27–35). http://hdl.handle.net/20.500.12708/198885
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Published in:
iPRA 2022 : The 4th Workshop on Interpolation: From Proofs to Applications : Book of Abstracts
-
Date (published):
Aug-2022
-
Event name:
iPRA 2022 - The 4th Workshop on Interpolation: From Proofs to Applications
en
Event date:
11-Aug-2022
-
Event place:
Haifa, Israel
-
Number of Pages:
9
-
Keywords:
Interference Proofs; Craig interpolation; SAT solving
en
Abstract:
Interference-based proof systems are necessary for proof generation in inprocessing SAT solvers. Unfortunately, their structure and semantic invariants are incompatible with standard recursive interpolant systems. Recent research on interference connects it with inference in more expressive logics. This circumvents some of the roadblocks in the quest for interpolant extraction from interference-based proofs, but also raises questions about the applicability of unfeasibility results in this setting.
en
Project title:
LogiCs-Stipendien: W1255-N23 (FWF) Heisenbugs: Auffindung und Erklärung: VRG11-005 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds)
-
Project (external):
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
