| ||||
| ||||
![]() Title:An Efficient Subsumption Test Pipeline for BS(LRA) Clauses Conference:IJCAR 2022 Tags:Bernays–Schönfinkel Fragment, Linear Arithmetic, Redundancy Elimination and Subsumption Abstract: The importance of subsumption testing for redundancy elimination in first-order logic automatic reasoning is well-known. Although the problem is already NP-complete for first-order clauses, the meanwhile developed test pipelines efficiently decide subsumption in almost all practical cases. We consider subsumption between first-oder clauses of the Bernays-Schönfinkel fragment over linear, real arithmetic constraints: BS(LRA). The bottleneck in this setup is deciding implication between the LRA constraints of two clauses. Our new sample point heuristic preempts expensive implication decisions in about 94% of all cases in benchmarks. Combined with filtering techniques for the first-order BS part of clauses, it results again in an efficient subsumption test pipeline for BS(LRA) clauses. An Efficient Subsumption Test Pipeline for BS(LRA) Clauses ![]() An Efficient Subsumption Test Pipeline for BS(LRA) Clauses | ||||
Copyright © 2002 – 2025 EasyChair |