Solving Quantified Modal Logic Problems by Translation to Classical Logics
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2022
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911570140856320 |
|---|---|
| author | Steen, Alexander Sutcliffe, Geoff Benzmüller, Christoph |
| author_facet | Steen, Alexander Sutcliffe, Geoff Benzmüller, Christoph |
| contents | This article describes an evaluation of Automated Theorem Proving (ATP) systems on problems taken from the QMLTP library of first-order modal logic problems. Principally, the problems are translated to both typed first-order and higher-order logic in the TPTP language using an embedding approach, and solved using first-order resp. higher-order logic ATP systems and model finders. Additionally, the results from native modal logic ATP systems are considered, and compared with the results from the embedding approach. The findings are that the embedding process is reliable and successful when state-of-the-art ATP systems are used as backend reasoners, The first-order and higher-order embeddings perform similarly, native modal logic ATP systems have comparable performance to classical systems using the embedding for proving theorems, native modal logic ATP systems are outperformed by the embedding approach for disproving conjectures, and the embedding approach can cope with a wider range of modal logics than the native modal systems considered. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2212_09570 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Solving Quantified Modal Logic Problems by Translation to Classical Logics Steen, Alexander Sutcliffe, Geoff Benzmüller, Christoph Logic in Computer Science Artificial Intelligence F.4.1; I.2.3 This article describes an evaluation of Automated Theorem Proving (ATP) systems on problems taken from the QMLTP library of first-order modal logic problems. Principally, the problems are translated to both typed first-order and higher-order logic in the TPTP language using an embedding approach, and solved using first-order resp. higher-order logic ATP systems and model finders. Additionally, the results from native modal logic ATP systems are considered, and compared with the results from the embedding approach. The findings are that the embedding process is reliable and successful when state-of-the-art ATP systems are used as backend reasoners, The first-order and higher-order embeddings perform similarly, native modal logic ATP systems have comparable performance to classical systems using the embedding for proving theorems, native modal logic ATP systems are outperformed by the embedding approach for disproving conjectures, and the embedding approach can cope with a wider range of modal logics than the native modal systems considered. |
| title | Solving Quantified Modal Logic Problems by Translation to Classical Logics |
| topic | Logic in Computer Science Artificial Intelligence F.4.1; I.2.3 |
| url | https://arxiv.org/abs/2212.09570 |