Knowledge Representation and Reasoning Seminar

From International Center for Computational Logic

Knowledge Representation and Reasoning Seminar

Course with SWS 0/2/0 (lecture/exercise/practical) in SS 2015

Lecturer

  • Steffen Hölldobler, Tobias Philipp

SWS

  • 0/2/0

Modules

Examination method

  • Oral exam
  • Seminar presentation

Proofs in Satisfiability Testing

The satisfiability problem (SAT) is one of the most prominent problems in theoretical computer science and has many applications in software verification, planning, bioinformatics or scheduling. Satisfiability solvers have become more complex in recent years due to inprocessing techniques and parallel computing. This raises the question whether the results of these solvers can be trusted. To gain confidence in the correctness of the results, SAT solvers can emit unsatisfiability proofs that can be validated using a checker.

The seminar will cover construction of proofs, verification of proofs, application of proofs, and considers the formal verification of checker systems.

The initial meeting is on 20.04.2015.

Duties of the Participants

The students are expected to participate in the seminar, write a short report of the assigned topic, and give a presentation in the end of the summer term. The presentation should have a length of 30 minutes, followed by a 15 minutes discussion.

German students can give the presentation also in German.

Topics

Allen Van Gelder
Verifying RUP Proofs of Propositional Unsatisfiability. ISAIM 2008
Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
Trimming while checking clausal proofs. FMCAD 2013: 181-188
Carsten Sinz, Armin Biere
Extended Resolution Proofs for Conjoining BDDs. CSR 2006
Anton Belov, Marijn Heule, João Marques-Silva
MUS Extraction Using Clausal Proofs. SAT 2014
Gurfinkel, A. ; Vizel, Y.
DRUPing for interpolates. FMCAD 2013
Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr.
Mechanical Verification of SAT Refutations with Extended Resolution. ITP 2013
Stephen A. Cook
A short proof of the pigeon hole principle using extended resolution
Feasiblz constructive proofs and the propositional calculus

Subscribe to events of this course (icalendar)

Seminar Initial Meeting; Research Talk by Steffen 'On Conditionals' DS2, April 20, 2015 in APB E005
Seminar Research Talk by Isara Anantavrasilp about 'Virus Classification' DS2, April 27, 2015 in APB E005
Seminar Research Talk by Tobias Philipp about 'Mechanically-Verified SAT Encodings of At-Most-k and PB-Constraints' DS1, May 4, 2015 in APB E005
Seminar Research Talk by Isara Anantavrasilp about 'Toward a Formal Model of Sequence Alignment Problem' DS2, May 18, 2015 in APB E005
Seminar Report by Sebastian Hahn about 'Modulogame' DS2, June 1, 2015 in APB E005
Seminar Research Talk by Christoph Wernhard about 'Second-Order Quantifier Elimination on Relational Monadic Formulas - A Basic Method and Some Less Expected Applications' DS2, June 8, 2015 in APB E005
Seminar Project Defense by Adrian Rebola Pardo about " Refutationally Complete Hierarchic Superposition Calculus with Definitions ", Master Thesis Report by Adrián Rebola Pardo about 'Unsatisfiability Proofs in Parity Reasoning' DS2, June 15, 2015 in APB E005
Seminar Project Defense by Luis Palacios on 'A Connectionist Model for Skeptical Abduction' and Asmaa Afeefy on 'Planning Problems and Fixpoint Semantics' DS2, June 22, 2015 in APB E005
Seminar Project Defense by Luis Palacios on 'A Connectionist Model for Skeptical Abduction' and Research Talk by Peter Steinke on 'PBLib - A Library For Encoding Pseudo-Boolean Constraints into CNF' DS2, June 29, 2015 in APB E005
Seminar CANCELD: Talk by Norbert Manthey on "The 'Parallel SAT' Research Project" DS2, July 6, 2015 in APB E005
Seminar Bachelor Defense by Sebastian Hahn on 'Modulospiel', Research Talk by Emmanuelle-Anna Dietz on 'A Computational Logic Approach to Syllogisms in Human Reasoning' DS2, July 13, 2015 in APB E2026
Seminar Research Talk by Sibylle Möhle on 'Propositional Model Counting and Enumeration' DS2, July 20, 2015 in APB E005


Calendar