A Mechanical Theorem Proving of First-Order Modal Logic (S5)

Atsuyuki SUZUKI; Kazumi NAKAMATSU

A Mechanical Theorem Proving of First-Order Modal Logic (S5)

Atsuyuki SUZUKI, Kazumi NAKAMATSU

Full Text Views

0

Cite this

Summary :

In this paper we have represented a model structure of modal lower (first-order) predicate logic (S5) (abbr. MLPC in our paper) in two-sorted extensional language (abbr. EL₂), and tried to translate a formula of MLPC into a formula of two-sorted logic (abbr. ELPC) in such a way as preserving provability. (i.e.P in MLPC iff P^* in ELPC, where P^* is the translation of P). Roughly speaking, modal symbol (necessity) is translated into the universal quantifier k of the domain which expresses the set of possible worlds, and n-ary predicates are n1 -ary predicates. For instance, xP (x) is translated into kx^*P^* (x^*, k), where ^* denotes the translation. Therefore it is possible to replace a theorem proving of MLPC with that of two-sorted logic ELPC, so we have shown it possible to prove a theorem of MLPC by using the resolution principle in ELPC. Then the completeness of the resolution in two-sorted logic is proved, and a normal form of MLPC is introduced. It is shown that for any formula of MLPC there exists an algorithm to transform the formula into its normal form. This normal form is obtained by decreasing the number of modal symbol in a formula as possible. For instance, xP (x) yQ (y) is transformed into xy (P (x) Q (y)).

Publication: IEICE TRANSACTIONS on transactions Vol.E65-E No.12 pp.730-736

Publication Date: 1982/12/25

Publicized

Online ISSN

DOI

Type of Manuscript: PAPER

Category: Mathematics

Authors

Atsuyuki SUZUKI
Kazumi NAKAMATSU

Keyword

Cite this

Copy

Atsuyuki SUZUKI, Kazumi NAKAMATSU, "A Mechanical Theorem Proving of First-Order Modal Logic (S5)" in IEICE TRANSACTIONS on transactions, vol. E65-E, no. 12, pp. 730-736, December 1982, doi: .
Abstract: In this paper we have represented a model structure of modal lower (first-order) predicate logic (S5) (abbr. MLPC in our paper) in two-sorted extensional language (abbr. EL₂), and tried to translate a formula of MLPC into a formula of two-sorted logic (abbr. ELPC) in such a way as preserving provability. (i.e.P in MLPC iff P^* in ELPC, where P^* is the translation of P). Roughly speaking, modal symbol (necessity) is translated into the universal quantifier k of the domain which expresses the set of possible worlds, and n-ary predicates are n1 -ary predicates. For instance, xP (x) is translated into kx^*P^* (x^*, k), where ^* denotes the translation. Therefore it is possible to replace a theorem proving of MLPC with that of two-sorted logic ELPC, so we have shown it possible to prove a theorem of MLPC by using the resolution principle in ELPC. Then the completeness of the resolution in two-sorted logic is proved, and a normal form of MLPC is introduced. It is shown that for any formula of MLPC there exists an algorithm to transform the formula into its normal form. This normal form is obtained by decreasing the number of modal symbol in a formula as possible. For instance, xP (x) yQ (y) is transformed into xy (P (x) Q (y)).
URL: https://global.ieice.org/en_transactions/transactions/10.1587/e65-e_12_730/_p

Copy

@ARTICLE{e65-e_12_730,
author={Atsuyuki SUZUKI, Kazumi NAKAMATSU, },
journal={IEICE TRANSACTIONS on transactions},
title={A Mechanical Theorem Proving of First-Order Modal Logic (S5)},
year={1982},
volume={E65-E},
number={12},
pages={730-736},
abstract={In this paper we have represented a model structure of modal lower (first-order) predicate logic (S5) (abbr. MLPC in our paper) in two-sorted extensional language (abbr. EL₂), and tried to translate a formula of MLPC into a formula of two-sorted logic (abbr. ELPC) in such a way as preserving provability. (i.e.P in MLPC iff P^* in ELPC, where P^* is the translation of P). Roughly speaking, modal symbol (necessity) is translated into the universal quantifier k of the domain which expresses the set of possible worlds, and n-ary predicates are n1 -ary predicates. For instance, xP (x) is translated into kx^*P^* (x^*, k), where ^* denotes the translation. Therefore it is possible to replace a theorem proving of MLPC with that of two-sorted logic ELPC, so we have shown it possible to prove a theorem of MLPC by using the resolution principle in ELPC. Then the completeness of the resolution in two-sorted logic is proved, and a normal form of MLPC is introduced. It is shown that for any formula of MLPC there exists an algorithm to transform the formula into its normal form. This normal form is obtained by decreasing the number of modal symbol in a formula as possible. For instance, xP (x) yQ (y) is transformed into xy (P (x) Q (y)).},
keywords={},
doi={},
ISSN={},
month={December},}

Copy

TY - JOUR
TI - A Mechanical Theorem Proving of First-Order Modal Logic (S5)
T2 - IEICE TRANSACTIONS on transactions
SP - 730
EP - 736
AU - Atsuyuki SUZUKI
AU - Kazumi NAKAMATSU
PY - 1982
DO -
JO - IEICE TRANSACTIONS on transactions
SN -
VL - E65-E
IS - 12
JA - IEICE TRANSACTIONS on transactions
Y1 - December 1982
AB - In this paper we have represented a model structure of modal lower (first-order) predicate logic (S5) (abbr. MLPC in our paper) in two-sorted extensional language (abbr. EL₂), and tried to translate a formula of MLPC into a formula of two-sorted logic (abbr. ELPC) in such a way as preserving provability. (i.e.P in MLPC iff P^* in ELPC, where P^* is the translation of P). Roughly speaking, modal symbol (necessity) is translated into the universal quantifier k of the domain which expresses the set of possible worlds, and n-ary predicates are n1 -ary predicates. For instance, xP (x) is translated into kx^*P^* (x^*, k), where ^* denotes the translation. Therefore it is possible to replace a theorem proving of MLPC with that of two-sorted logic ELPC, so we have shown it possible to prove a theorem of MLPC by using the resolution principle in ELPC. Then the completeness of the resolution in two-sorted logic is proved, and a normal form of MLPC is introduced. It is shown that for any formula of MLPC there exists an algorithm to transform the formula into its normal form. This normal form is obtained by decreasing the number of modal symbol in a formula as possible. For instance, xP (x) yQ (y) is transformed into xy (P (x) Q (y)).
ER -