Saturation-Based Uniform Interpolation for Multi-Modal Logics

Ruba Alassaf; Renate A. Schmidt; Uli Sattler

Saturation-Based Uniform Interpolation for Multi-Modal Logics

Ruba Alassaf, Renate A. Schmidt, Uli Sattler

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

Abstract

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 K_n. 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.

Original language	English
Title of host publication	Advances in Modal Logic
Editors	David Fernandez-Duque, Alessandra Palmigiano, Sophie Pinchinat
Publisher	College Publications
Pages	37-57
Number of pages	21
ISBN (Electronic)	9781848904132
Publication status	Published - 19 Jul 2022
Event	14th Conference on Advances in Modal Logic, AiML 2022 - Rennes, France Duration: 22 Aug 2022 → 25 Aug 2022

Publication series

Name	Advances in Modal Logic
Volume	14

Conference

Conference	14th Conference on Advances in Modal Logic, AiML 2022
Country/Territory	France
City	Rennes
Period	22/08/22 → 25/08/22

Keywords

bisimulations
resolution
uniform interpolation

Cite this

@inproceedings{0b358a3f6c464c098c0d2569906c27bd,

title = "Saturation-Based Uniform Interpolation for Multi-Modal Logics",

abstract = "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.",

keywords = "bisimulations, resolution, uniform interpolation",

author = "Ruba Alassaf and Schmidt, \{Renate A.\} and Uli Sattler",

year = "2022",

month = jul,

day = "19",

language = "English",

series = "Advances in Modal Logic",

publisher = "College Publications",

pages = "37--57",

editor = "David Fernandez-Duque and Alessandra Palmigiano and Sophie Pinchinat",

booktitle = "Advances in Modal Logic",

address = "United Kingdom",

}

Saturation-Based Uniform Interpolation for Multi-Modal Logics. / Alassaf, Ruba; Schmidt, Renate A.; Sattler, Uli.
Advances in Modal Logic. ed. / David Fernandez-Duque; Alessandra Palmigiano; Sophie Pinchinat. College Publications, 2022. p. 37-57 (Advances in Modal Logic; Vol. 14).

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Saturation-Based Uniform Interpolation for Multi-Modal Logics

AU - Alassaf, Ruba

AU - Schmidt, Renate A.

AU - Sattler, Uli

PY - 2022/7/19

Y1 - 2022/7/19

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 - https://www.scopus.com/pages/publications/85184346700

M3 - Conference contribution

AN - SCOPUS:85184346700

T3 - Advances in Modal Logic

SP - 37

EP - 57

BT - Advances in Modal Logic

A2 - Fernandez-Duque, David

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 -

Saturation-Based Uniform Interpolation for Multi-Modal Logics

Abstract

Publication series

Conference

Keywords

Other files and links

Fingerprint

Cite this