Expressing Dung's Extensions as FO-Formulas to Enumerate Them with an SMT Solver (Model theoretic aspects of the notion of independence and dimension)

機関リポジトリ (HANDLE) オープンアクセス

この論文をさがす

説明

It is useful to express constraints for Dung's extensions as FO-formulas so that we can enumerate extensions with an SMT solver. We can extract an extension with a naive SMT solver if we naively express constraints for extensions as FO-formulas. But the definitions of some extensions require maximality /minimality conditions that can not be expressed as FO-formulas. On the other hand, a naive expression is readable but sometimes hard to solve with an SMT solver. Moreover, we need to improve a naive SMT solver to enumerate extensions since an enumeration is an iteration of an extraction. In this paper, we propose a method to enumerate Dung's extensions by solving a Partial Maximal Satisfiable Subsets Enumeration problem, which is an extension of a Maximal Satisfiable Subsets Enumeration problem[l]. In particular, we express hard constraints and soft constraints, which are required for a Partial Maximal Satisfiable Subsets Enumeration problem, with FO-formulas.

収録刊行物

詳細情報 詳細情報について

  • CRID
    1050850092155962752
  • NII書誌ID
    AN00061013
  • ISSN
    18802818
  • HANDLE
    2433/261565
  • 本文言語コード
    en
  • 資料種別
    departmental bulletin paper
  • データソース種別
    • IRDB

問題の指摘

ページトップへ