[Back]

G. Reger, M. Suda:
"Global Subsumption Revisited (Briefly)";
in: "Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, Coimbra, Portugal, July 2, 2016.", 44; issued by: Laura Kovács and Andrei Voronkov; EasyChair EPiC Series in Computing, 2017, 61 - 73.

Global subsumption is an existing simplification technique for saturation-based first-order theorem provers. The general idea is that we can replace a clause C by its subclause D if D follows from the initial problem as D will subsume C. The effectiveness of the technique comes from a cheap, global approach for (incompletely) checking whether D is a consequence of the initial problem. The idea is to produce and maintain a set S of ground clauses that follow from the input (e.g. grounded versions of all derived clauses) and to check whether a grounding of D follows from this set. As this is now a propositional problem this check can be performed by a SAT solver, making it efficient. In this paper we review the global subsumption technique and pose a number of questions related to the practical implementation of global subsumption and possible variations of the approach. We consider, for example, which groundings to place in S, how to select the subclause(s) D to check, how to integrate this technique with the AVATAR approach and whether it makes sense to replace the SAT solver with an SMT solver. This discussion takes place within the context of the Vampire theorem prover.

first-order logic, theorem proving, Vampire

http://publik.tuwien.ac.at/files/publik_264592.pdf