Implementing Lexicographic Inference Using Partial MaxSAT
摘要
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.