Talks and Poster Presentations (without Proceedings-Entry):
A. Biere, B. Kiesl, M. Seidl, M. Suda:
"Blocked clauses in first-order logic";
Talk: The Third Vampire Workshop, VAMPIRE 2016,
A wide number of effective clause-elimination procedures for SAT is based on the clause-redundancy property called blocked clauses. In this paper, we introduce a generalization of blocked clauses to first-order logic and show how they can be used in a preprocessing step within an automated theorem prover. We report on experimental results obtained from a prototype implementation in Vampire.
First-order logic, blocked clauses
Created from the Publication Database of the Vienna University of Technology.