Knowledge Representation and Reasoning Seminar
Knowledge Representation and Reasoning Seminar
Course with SWS 0/2/0 (lecture/exercise/practical) in SS 2015
Lecturer
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
