[Back]


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, Coimbra, Portugal; 2016-07-02.



English abstract:
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.

Keywords:
First-order logic, blocked clauses

Created from the Publication Database of the Vienna University of Technology.