Xinran Ning

Set-Blocked Clause and Extended Set-Blocked Clause in First-Order Logic

2018 · Symmetry

Due to scale and complexity of first-order formulas, simplifications play a very important role in first-order theorem proving, in which removal of clauses and literals identified as redundant is a significant component. In this paper, …