Non-clausal multi-ary alpha-generalized resolution calculus for a finite lattice-valued logic

Yang Xu, J. Liu, Xingxing He, Xiaomei Zhong, Shuwei Chen

Research output: Contribution to journalArticle

Abstract

Due to the need of the logical foundation for uncertain information processing, development of efficient automated reasoning system based on non-classical logics is always an active research area. The present paper focuses on the resolution-based automated reasoning theory in a many-valued logic with truth-values defined in a lattice-ordered many-valued algebraic structure - lattice implication algebras (LIA). Specifically, as a continuation and extension of the established work on binary resolution at a certain truth-value level α (called α-resolution), a non-clausal multi-ary α-generalized resolution calculus is introduced for a lattice-valued propositional logic LP(X) based on LIA, which is essentially a non-clausal generalized resolution avoiding reduction to normal clausal form. The new resolution calculus in LP(X) is then proved to be sound and complete. The concepts and theoretical results are further extended and established in the corresponding lattice-valued first-order logic LF(X) based on LIA.
LanguageEnglish
Pages384-401
Number of pages18
JournalInternational Journal of Computational Intelligence Systems
Volume11
Issue number1
DOIs
Publication statusPublished - 15 Jan 2018

Fingerprint

Algebra
Calculus
Logic
Many valued logics
Automated Reasoning
Acoustic waves
Non-classical Logics
Many valued
Many-valued Logic
Propositional Logic
First-order Logic
Algebraic Structure
Information Processing
Normal Form
Continuation
Binary
Truth

Keywords

  • Automated reasoning
  • Resolution principle
  • Lattice-valued logic

Cite this

@article{6aa773b8e8e84b548ec5e1f2ff4f90bb,
title = "Non-clausal multi-ary alpha-generalized resolution calculus for a finite lattice-valued logic",
abstract = "Due to the need of the logical foundation for uncertain information processing, development of efficient automated reasoning system based on non-classical logics is always an active research area. The present paper focuses on the resolution-based automated reasoning theory in a many-valued logic with truth-values defined in a lattice-ordered many-valued algebraic structure - lattice implication algebras (LIA). Specifically, as a continuation and extension of the established work on binary resolution at a certain truth-value level α (called α-resolution), a non-clausal multi-ary α-generalized resolution calculus is introduced for a lattice-valued propositional logic LP(X) based on LIA, which is essentially a non-clausal generalized resolution avoiding reduction to normal clausal form. The new resolution calculus in LP(X) is then proved to be sound and complete. The concepts and theoretical results are further extended and established in the corresponding lattice-valued first-order logic LF(X) based on LIA.",
keywords = "Automated reasoning, Resolution principle, Lattice-valued logic",
author = "Yang Xu and J. Liu and Xingxing He and Xiaomei Zhong and Shuwei Chen",
year = "2018",
month = "1",
day = "15",
doi = "10.2991/ijcis.11.1.29",
language = "English",
volume = "11",
pages = "384--401",
journal = "International Journal of Computational Intelligence Systems",
issn = "1875-6891",
number = "1",

}

Non-clausal multi-ary alpha-generalized resolution calculus for a finite lattice-valued logic. / Xu, Yang; Liu, J.; He, Xingxing; Zhong, Xiaomei; Chen, Shuwei.

In: International Journal of Computational Intelligence Systems, Vol. 11, No. 1, 15.01.2018, p. 384-401.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Non-clausal multi-ary alpha-generalized resolution calculus for a finite lattice-valued logic

AU - Xu, Yang

AU - Liu, J.

AU - He, Xingxing

AU - Zhong, Xiaomei

AU - Chen, Shuwei

PY - 2018/1/15

Y1 - 2018/1/15

N2 - Due to the need of the logical foundation for uncertain information processing, development of efficient automated reasoning system based on non-classical logics is always an active research area. The present paper focuses on the resolution-based automated reasoning theory in a many-valued logic with truth-values defined in a lattice-ordered many-valued algebraic structure - lattice implication algebras (LIA). Specifically, as a continuation and extension of the established work on binary resolution at a certain truth-value level α (called α-resolution), a non-clausal multi-ary α-generalized resolution calculus is introduced for a lattice-valued propositional logic LP(X) based on LIA, which is essentially a non-clausal generalized resolution avoiding reduction to normal clausal form. The new resolution calculus in LP(X) is then proved to be sound and complete. The concepts and theoretical results are further extended and established in the corresponding lattice-valued first-order logic LF(X) based on LIA.

AB - Due to the need of the logical foundation for uncertain information processing, development of efficient automated reasoning system based on non-classical logics is always an active research area. The present paper focuses on the resolution-based automated reasoning theory in a many-valued logic with truth-values defined in a lattice-ordered many-valued algebraic structure - lattice implication algebras (LIA). Specifically, as a continuation and extension of the established work on binary resolution at a certain truth-value level α (called α-resolution), a non-clausal multi-ary α-generalized resolution calculus is introduced for a lattice-valued propositional logic LP(X) based on LIA, which is essentially a non-clausal generalized resolution avoiding reduction to normal clausal form. The new resolution calculus in LP(X) is then proved to be sound and complete. The concepts and theoretical results are further extended and established in the corresponding lattice-valued first-order logic LF(X) based on LIA.

KW - Automated reasoning

KW - Resolution principle

KW - Lattice-valued logic

U2 - 10.2991/ijcis.11.1.29

DO - 10.2991/ijcis.11.1.29

M3 - Article

VL - 11

SP - 384

EP - 401

JO - International Journal of Computational Intelligence Systems

T2 - International Journal of Computational Intelligence Systems

JF - International Journal of Computational Intelligence Systems

SN - 1875-6891

IS - 1

ER -