A Heuristic Proof Procedure for First-Order Logic
Summary :
Inspired by the efficient proof procedures discussed in Computability logic [3],[5],[6], we describe a heuristic proof procedure for first-order logic. This is a variant of Gentzen sequent system [2] and has the following features: (a) it views sequents as games between the machine and the environment, and (b) it views proofs as a winning strategy of the machine. From this game-based viewpoint, a poweful heuristic can be extracted and a fair degree of determinism in proof search can be obtained. This article proposes a new deductive system LKg with respect to first-order logic and proves its soundness and completeness.
- Publication
- IEICE TRANSACTIONS on Information Vol.E103-D No.3 pp.549-552
- Publication Date
- 2020/03/01
- Publicized
- 2019/11/21
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.2019FCL0003
- Type of Manuscript
- Special Section LETTER (Special Section on Foundations of Computer Science — Frontiers of Theory of Computation and Algorithm —)
- Category
Authors
Keehang KWON
DongA University
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Keehang KWON, "A Heuristic Proof Procedure for First-Order Logic" in IEICE TRANSACTIONS on Information,
vol. E103-D, no. 3, pp. 549-552, March 2020, doi: 10.1587/transinf.2019FCL0003.
Abstract: Inspired by the efficient proof procedures discussed in Computability logic [3],[5],[6], we describe a heuristic proof procedure for first-order logic. This is a variant of Gentzen sequent system [2] and has the following features: (a) it views sequents as games between the machine and the environment, and (b) it views proofs as a winning strategy of the machine. From this game-based viewpoint, a poweful heuristic can be extracted and a fair degree of determinism in proof search can be obtained. This article proposes a new deductive system LKg with respect to first-order logic and proves its soundness and completeness.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2019FCL0003/_p
Copy
@ARTICLE{e103-d_3_549,
author={Keehang KWON, },
journal={IEICE TRANSACTIONS on Information},
title={A Heuristic Proof Procedure for First-Order Logic},
year={2020},
volume={E103-D},
number={3},
pages={549-552},
abstract={Inspired by the efficient proof procedures discussed in Computability logic [3],[5],[6], we describe a heuristic proof procedure for first-order logic. This is a variant of Gentzen sequent system [2] and has the following features: (a) it views sequents as games between the machine and the environment, and (b) it views proofs as a winning strategy of the machine. From this game-based viewpoint, a poweful heuristic can be extracted and a fair degree of determinism in proof search can be obtained. This article proposes a new deductive system LKg with respect to first-order logic and proves its soundness and completeness.},
keywords={},
doi={10.1587/transinf.2019FCL0003},
ISSN={1745-1361},
month={March},}
Copy
TY - JOUR
TI - A Heuristic Proof Procedure for First-Order Logic
T2 - IEICE TRANSACTIONS on Information
SP - 549
EP - 552
AU - Keehang KWON
PY - 2020
DO - 10.1587/transinf.2019FCL0003
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E103-D
IS - 3
JA - IEICE TRANSACTIONS on Information
Y1 - March 2020
AB - Inspired by the efficient proof procedures discussed in Computability logic [3],[5],[6], we describe a heuristic proof procedure for first-order logic. This is a variant of Gentzen sequent system [2] and has the following features: (a) it views sequents as games between the machine and the environment, and (b) it views proofs as a winning strategy of the machine. From this game-based viewpoint, a poweful heuristic can be extracted and a fair degree of determinism in proof search can be obtained. This article proposes a new deductive system LKg with respect to first-order logic and proves its soundness and completeness.
ER -
English
