Vorträge und Posterpräsentationen (ohne Tagungsband-Eintrag):
A. Biere, B. Kiesl, M. Seidl, M. Suda:
"Blocked clauses in first-order logic";
Vortrag: The Third Vampire Workshop, VAMPIRE 2016,
Coimbra, Portugal;
02.07.2016.
Kurzfassung englisch:
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.
Schlagworte:
First-order logic, blocked clauses
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.