This paper introduces the online reasoning platform InfOCF-Web 2.0 that provides easy access to implementations of various inference methods for conditional belief bases. We present an overview of the realization of the inductive inference operator s p-entailment, system Z, c-inference, and system W. In order to address the fact that the possible worlds to be taken into account grow exponentially with the propositional signature over which the conditionals in the belief base are defined, the implementations employ SAT and Partial MaxSAT concepts and use the power of current SAT and SMT solvers. Our evaluation shows that each of the four inference operators can handle belief bases over signatures containing more than 100 variables and with more than 100 conditionals. Thus, InfOCF-Web 2.0 scales up nonmonotonic reasoning from conditionals to a new dimension because apart from the implementations now available in InfOCF-Web 2.0, there is no other implementation of an inference operator for conditional belief bases for which such problem sizes are feasible.

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

Scaling Up Reasoning from Conditional Belief Bases

  • Christoph Beierle,
  • Jonas Haldimann,
  • Arthur Sanin,
  • Leon Schwarzer,
  • Aron Spang,
  • Lars-Phillip Spiegel,
  • Martin von Berg

摘要

This paper introduces the online reasoning platform InfOCF-Web 2.0 that provides easy access to implementations of various inference methods for conditional belief bases. We present an overview of the realization of the inductive inference operator s p-entailment, system Z, c-inference, and system W. In order to address the fact that the possible worlds to be taken into account grow exponentially with the propositional signature over which the conditionals in the belief base are defined, the implementations employ SAT and Partial MaxSAT concepts and use the power of current SAT and SMT solvers. Our evaluation shows that each of the four inference operators can handle belief bases over signatures containing more than 100 variables and with more than 100 conditionals. Thus, InfOCF-Web 2.0 scales up nonmonotonic reasoning from conditionals to a new dimension because apart from the implementations now available in InfOCF-Web 2.0, there is no other implementation of an inference operator for conditional belief bases for which such problem sizes are feasible.