## Abstract

In the present paper, as a continuous work about α-resolution principle based on lattice-valued propositional logic LP(X) (Information Sciences 130 (2000) 1-29) whose algebra of truth-values is a relatively general lattice - lattice implication algebra (LIA), the lattice-valued resolution principle for the corresponding first-order lattice-valued logic system LF(X) is focused. Firstly, some concepts about lattice-valued resolution principle for LF(X) are introduced and the Herbrand theorem for LF(X) is proved. Then, an α-resolution principle, which can be used to judge if a first-order lattice-valued logical formula in LF(X) is false at a truth-valued level α (i.e., α-false), is established. Finally, the completeness theorem of this α-resolution principle and the soundness theorem for the strong α-resolution are also proved. It is hoped that the current work would serve as a foundation for constructing resolution-based automated reasoning methods for lattice-valued logic capable of dealing with both comparable and incomparable uncertain information.

Original language | English |
---|---|

Pages (from-to) | 221-239 |

Number of pages | 19 |

Journal | Information Sciences |

Volume | 132 |

Issue number | 1-4 |

DOIs | |

State | Published - Feb 2001 |

### Funding

This work was partially supported by the National Natural Science Foundation of People's Republic of China (Grant No. 60074014).

Funders | Funder number |
---|---|

Not added | 60074014 |

## ASJC Scopus subject areas

- Software
- Control and Systems Engineering
- Theoretical Computer Science
- Computer Science Applications
- Information Systems and Management
- Artificial Intelligence