2 papers
cs.LO2019
Partial Quantifier Elimination With Learning
Eugene Goldberg
We consider a modification of the Quantifier Elimination (QE) problem called Partial QE (PQE). In PQE, only a small part of the formula is taken out of the scope of quantifiers. Th…
cs.LO2012
Checking Satisfiability by Dependency Sequents
Eugene Goldberg, Panagiotis Manolios
We introduce a new algorithm for checking satisfiability based on a calculus of Dependency sequents (D-sequents). Given a CNF formula F(X), a D-sequent is a record stating that und…