A General Proof Method for First-Order Modal Logic
Abstract
We present a general sequent-based proof method for first-order modal logics in which the Barcan formula holds. The most important feature of our system is the fact that it has identical inference rules for every modal logic; different modal logics can be obtained by changing the conditions under which two formulas are allowed to resolve against each other It is argued that the proof method is very natural because these conditions correspond to the conditions on the accessibility relation in Kripke semantics. I
Cite
Text
Jackson and Reichgelt. "A General Proof Method for First-Order Modal Logic." International Joint Conference on Artificial Intelligence, 1987.Markdown
[Jackson and Reichgelt. "A General Proof Method for First-Order Modal Logic." International Joint Conference on Artificial Intelligence, 1987.](https://mlanthology.org/ijcai/1987/jackson1987ijcai-general/)BibTeX
@inproceedings{jackson1987ijcai-general,
title = {{A General Proof Method for First-Order Modal Logic}},
author = {Jackson, Peter and Reichgelt, Han},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1987},
pages = {942-944},
url = {https://mlanthology.org/ijcai/1987/jackson1987ijcai-general/}
}