LogiCS | Benjamin Kiesl

Project Assistant
Knowledge-Based Systems Group
Institute of Logic and Computation
TU Wien
Favoritenstraße 9-11, 1040 Wien, Austria
Room: Lab 2, 3rd Floor
Phone: +43 1 58801 192414
E-Mail: kiesl [at] kr.tuwien.ac.at

Research Interests

Automated Reasoning (in particular SAT solving, QSAT solving, and First-Order Theorem Proving)
Knowledge Representation
Logic Programming (in particular Answer-Set Programming)

Current Position

I am a PhD student fully funded by the Doctoral College Logical Methods in Computer Science at TU Wien. My supervisors are Martina Seidl and Hans Tompits.

Education

TU Wien
Master's Program in Computational Intelligence

Tools

drat2er - A command-line tool that transforms DRAT proofs (as produced by modern SAT solvers) into extended-resolution proofs.

Publications

Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere (2018):
Local Redundancy in SAT: Generalizations of Blocked Clauses.
In: Logical Methods in Computer Science (LMCS), vol. 14(4:3).
.
Benjamin Kiesl, Adrian Rebola-Pardo, and Marijn J.H. Heule (2018):
Extended Resolution Simulates DRAT.
In: Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018). Best Paper Award.
.
Marijn J.H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere (2017):
PRuning Through Satisfaction.
In: Proceedings of the 13th Haifa Verification Conference (HVC 2017). Best Paper Award.
.
Benjamin Kiesl, Marijn J.H. Heule, and Martina Seidl (2017):
A Little Blocked Literal Goes a Long Way.
In: Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT 2017).
.
Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere (2017):
Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood?
In: Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI 2017).
.
Benjamin Kiesl and Martin Suda (2017):
A Unifying Principle for Clause Elimination in First-Order Logic.
In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26). Best Paper Award.
.
Marijn J.H. Heule, Benjamin Kiesl, and Armin Biere (2017):
Short Proofs Without New Variables.
In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26). Best Paper Award.
.
Marijn J.H. Heule and Benjamin Kiesl (2017):
The Potential of Interference-Based Proof Systems.
In: Proceedings of the 1st ARCADE Workshop (ARCADE 2017).
.
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, and Armin Biere (2017):
Blocked Clauses in First-Order Logic.
In: Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21).
.
Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere (2016):
Super-Blocked Clauses.
In: Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016).
.
Benjamin Kiesl, Peter Schüller, and Hans Tompits (2015):
On Structural Analysis of Non-Ground Answer-Set Programs.
In: Proceedings of the Technical Communications of the 31st International Conference on Logic Programming (ICLP 2015).