TY - GEN
T1 - Saturation-Based Uniform Interpolation for Multi-Modal Logics
AU - Alassaf, Ruba
AU - Schmidt, Renate A.
AU - Sattler, Uli
N1 - Publisher Copyright:
© 2022 College Publications. All rights reserved.
PY - 2022
Y1 - 2022
N2 - Uniform interpolation has been the subject of many recent research papers due to its link to Craig interpolation and its potential use in knowledge-based and agent-based systems. In this paper, we present a saturation-based system that computes a local uniform interpolant for a formula and a “keep” signature in the multi-modal logic Kn. The system works by exhaustively applying a set of rules to generate a sufficient number of local consequences, which are then filtered to remove those that contain symbols outside the keep signature. We show that the system is guaranteed to terminate and is sound and uniform interpolation complete.
AB - Uniform interpolation has been the subject of many recent research papers due to its link to Craig interpolation and its potential use in knowledge-based and agent-based systems. In this paper, we present a saturation-based system that computes a local uniform interpolant for a formula and a “keep” signature in the multi-modal logic Kn. The system works by exhaustively applying a set of rules to generate a sufficient number of local consequences, which are then filtered to remove those that contain symbols outside the keep signature. We show that the system is guaranteed to terminate and is sound and uniform interpolation complete.
KW - Bisimulations
KW - Resolution
KW - Uniform Interpolation
UR - http://www.scopus.com/inward/record.url?scp=85184346700&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:85184346700
T3 - Advances in Modal Logic
SP - 37
EP - 57
BT - Advances in Modal Logic, AiML 2022
A2 - Fernandez-Duque, David
A2 - Palmigiano, Alessandra
A2 - Palmigiano, Alessandra
A2 - Pinchinat, Sophie
PB - College Publications
T2 - 14th Conference on Advances in Modal Logic, AiML 2022
Y2 - 22 August 2022 through 25 August 2022
ER -