Alpha-satisfiability and alpha-lock resolution for a lattice-valued logic LP(X)

Research output: Contribution to report/book/conference proceedingsIn-proceedings paper

Authors

  • Xingxing He
  • Yang Xu
  • Yingfang Li
  • Jun Liu
  • Luis Martinez
  • Da Ruan

Documents & links

Abstract

This paper focuses on some automated reasoning issues for a kind of lattice-valued logic LP(X) based on lattice-valued algebra. Firstly some extended strategies from classical logic to LP(X) are investigated in order to verify theAlpha-satisability of formulae in LP(X) while the main focus is given on the role of constant formula played in LP(X) in order to simply the verication procedure in the semantic level. Then, an alpha-lock resolution method in LP(X) is proposed and the weak completeness of this method is proved. The work will provide a support for the more e±cient resolution based automated reasoning in LP(X).

Details

Original languageEnglish
Title of host publicationHybrid Artificial Intelligence Systems
Place of PublicationHeidelberg, Germany
Pages320-327
Volume2
Publication statusPublished - Jun 2010
EventHybrid Artificial Intelligence Systems - 5th International Conference HAIS2010, San Sebastián, Spain
Duration: 23 Jun 201025 Jun 2010

Publication series

NameLecture Notes in Artificial Intelligence
Number6077

Conference

ConferenceHybrid Artificial Intelligence Systems
CountrySpain
CitySan Sebastián
Period2010-06-232010-06-25

Keywords

  • lattice-valued logic, Alpha-resolution principle, Alpha-satisability, ALpha-lock resolution method

ID: 60722