Lehman’s lexicographic inference is one of the established inference operators for reasoning from conditional belief bases that satisfies many properties desirable for nonmonotonic reasoning. In contrast to its well investigated formal properties, implementations of lexicographic inference are rare. In this paper, we introduce the algorithm LEXinf for realizing lexicographic inference using a MaxSAT solver. We prove the correctness of the algorithm and demonstrate the feasibility and efficiency of our approach by implementing it using Python and the state-of-the-art solver Z3. We empirically evaluate the implementation and compare it to implementations of other inference operators.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Implementing Lexicographic Inference Using Partial MaxSAT

  • Jonas Haldimann,
  • Aron Spang,
  • Lars-Phillip Spiegel,
  • Christoph Beierle

摘要

Lehman’s lexicographic inference is one of the established inference operators for reasoning from conditional belief bases that satisfies many properties desirable for nonmonotonic reasoning. In contrast to its well investigated formal properties, implementations of lexicographic inference are rare. In this paper, we introduce the algorithm LEXinf for realizing lexicographic inference using a MaxSAT solver. We prove the correctness of the algorithm and demonstrate the feasibility and efficiency of our approach by implementing it using Python and the state-of-the-art solver Z3. We empirically evaluate the implementation and compare it to implementations of other inference operators.