Automatic Theorem Proving for Modal Predicate Logic

Kazumi NAKAMATSU; Atsuyuki SUZUKI

Automatic Theorem Proving for Modal Predicate Logic

Kazumi NAKAMATSU, Atsuyuki SUZUKI

Full Text Views

0

Cite this

Summary :

In this paper we give an algorithm of automatic theorem proving for various modal predicate systems, and prove its completeness. These modal systems can be tanslated into two-sorted extensional system. Using this fact, the theorem proving can be implemented by using the resolution for the extensional systems. Especially our new results in this paper are two inference rules for S4-modal system, which give a shorter proof than the ordinary resolution.

Publication: IEICE TRANSACTIONS on transactions Vol.E67-E No.4 pp.203-210

Publication Date: 1984/04/25

Publicized

Online ISSN

DOI

Type of Manuscript: PAPER

Category: Communication Theory

Authors

Kazumi NAKAMATSU
Atsuyuki SUZUKI

Keyword

Cite this

Copy

Kazumi NAKAMATSU, Atsuyuki SUZUKI, "Automatic Theorem Proving for Modal Predicate Logic" in IEICE TRANSACTIONS on transactions, vol. E67-E, no. 4, pp. 203-210, April 1984, doi: .
Abstract: In this paper we give an algorithm of automatic theorem proving for various modal predicate systems, and prove its completeness. These modal systems can be tanslated into two-sorted extensional system. Using this fact, the theorem proving can be implemented by using the resolution for the extensional systems. Especially our new results in this paper are two inference rules for S4-modal system, which give a shorter proof than the ordinary resolution.
URL: https://global.ieice.org/en_transactions/transactions/10.1587/e67-e_4_203/_p

Copy

@ARTICLE{e67-e_4_203,
author={Kazumi NAKAMATSU, Atsuyuki SUZUKI, },
journal={IEICE TRANSACTIONS on transactions},
title={Automatic Theorem Proving for Modal Predicate Logic},
year={1984},
volume={E67-E},
number={4},
pages={203-210},
abstract={In this paper we give an algorithm of automatic theorem proving for various modal predicate systems, and prove its completeness. These modal systems can be tanslated into two-sorted extensional system. Using this fact, the theorem proving can be implemented by using the resolution for the extensional systems. Especially our new results in this paper are two inference rules for S4-modal system, which give a shorter proof than the ordinary resolution.},
keywords={},
doi={},
ISSN={},
month={April},}

Copy

TY - JOUR
TI - Automatic Theorem Proving for Modal Predicate Logic
T2 - IEICE TRANSACTIONS on transactions
SP - 203
EP - 210
AU - Kazumi NAKAMATSU
AU - Atsuyuki SUZUKI
PY - 1984
DO -
JO - IEICE TRANSACTIONS on transactions
SN -
VL - E67-E
IS - 4
JA - IEICE TRANSACTIONS on transactions
Y1 - April 1984
AB - In this paper we give an algorithm of automatic theorem proving for various modal predicate systems, and prove its completeness. These modal systems can be tanslated into two-sorted extensional system. Using this fact, the theorem proving can be implemented by using the resolution for the extensional systems. Especially our new results in this paper are two inference rules for S4-modal system, which give a shorter proof than the ordinary resolution.
ER -