Redundancy elimination is one of the crucial ingredients of efficient saturation-based proof search. We strengthen redundancy elimination by introducing a new notion of redundancy, based on partial clauses and redundancy formulas. The new notion allows us to recognize redundant clauses and inferences that cannot be recognized by standard redundancy elimination criteria. In a way, our notion blurs the distinction between redundancy at the level of inferences and redundancy at the level of clauses. We present a superposition calculus PaRC on partial clauses and prove that it is refutationally complete. We discuss the implementation of the calculus in the theorem prover Vampire. Our experiments show the power of the new approach: we were able to solve 24 TPTP problems not previously solved by any prover, including previous versions of Vampire.

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

Partial Redundancy in Saturation

  • Márton Hajdu,
  • Laura Kovács,
  • Andrei Voronkov

摘要

Redundancy elimination is one of the crucial ingredients of efficient saturation-based proof search. We strengthen redundancy elimination by introducing a new notion of redundancy, based on partial clauses and redundancy formulas. The new notion allows us to recognize redundant clauses and inferences that cannot be recognized by standard redundancy elimination criteria. In a way, our notion blurs the distinction between redundancy at the level of inferences and redundancy at the level of clauses. We present a superposition calculus PaRC on partial clauses and prove that it is refutationally complete. We discuss the implementation of the calculus in the theorem prover Vampire. Our experiments show the power of the new approach: we were able to solve 24 TPTP problems not previously solved by any prover, including previous versions of Vampire.