Algorithmic correspondence and analytic rules
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_ | 1866916689318248448 |
|---|---|
| author | De Domenico, Andrea Greco, Giuseppe Palmigiano, Alessandra |
| author_facet | De Domenico, Andrea Greco, Giuseppe Palmigiano, Alessandra |
| contents | We introduce the algorithm MASSA which takes classical modal formulas in input, and, when successful, effectively generates: (a) (analytic) geometric rules of the labelled calculus G3K, and (b) cut-free derivations (of a certain `canonical' shape) of each given input formula in the geometric labelled calculus obtained by adding the rule in output to G3K. We show that MASSA successfully terminates whenever its input formula is a (definite) analytic inductive formula, in which case, the geometric axiom corresponding to the output rule is, modulo logical equivalence, the first-order correspondent of the input formula. In proving the correctness of MASSA, we also show that the algorithm for the elimination of second-order quantifiers SCAN is complete with respect to the class of inductive analytic formulas. Finally, we show how our algorithm can be extended to the class of inductive formulas and to modal logic with quantifiers. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2203_14147 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Algorithmic correspondence and analytic rules De Domenico, Andrea Greco, Giuseppe Palmigiano, Alessandra Logic Logic in Computer Science 03B35, 03B45, 06D10, 06D50, 03F03, 03F05, 03F07, 03G10 We introduce the algorithm MASSA which takes classical modal formulas in input, and, when successful, effectively generates: (a) (analytic) geometric rules of the labelled calculus G3K, and (b) cut-free derivations (of a certain `canonical' shape) of each given input formula in the geometric labelled calculus obtained by adding the rule in output to G3K. We show that MASSA successfully terminates whenever its input formula is a (definite) analytic inductive formula, in which case, the geometric axiom corresponding to the output rule is, modulo logical equivalence, the first-order correspondent of the input formula. In proving the correctness of MASSA, we also show that the algorithm for the elimination of second-order quantifiers SCAN is complete with respect to the class of inductive analytic formulas. Finally, we show how our algorithm can be extended to the class of inductive formulas and to modal logic with quantifiers. |
| title | Algorithmic correspondence and analytic rules |
| topic | Logic Logic in Computer Science 03B35, 03B45, 06D10, 06D50, 03F03, 03F05, 03F07, 03G10 |
| url | https://arxiv.org/abs/2203.14147 |