Knowledge Representation and Reasoning Seminar
Knowledge Representation and Reasoning Seminar
Lehrveranstaltung mit SWS 0/2/0 (Vorlesung/Übung/Praktikum) in SS 2015
Dozent
- Steffen Hölldobler
- Tobias Philipp
Umfang (SWS)
- 0/2/0
Module
Leistungskontrolle
- Mündliche Prüfung
- Referat
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
Veranstaltungskalender abonnieren (icalendar)
| Seminar | Initial Meeting; Research Talk by Steffen 'On Conditionals' | DS2, 20. April 2015 in APB E005 | |
| Seminar | Research Talk by Isara Anantavrasilp about 'Virus Classification' | DS2, 27. April 2015 in APB E005 | |
| Seminar | Research Talk by Tobias Philipp about 'Mechanically-Verified SAT Encodings of At-Most-k and PB-Constraints' | DS1, 4. Mai 2015 in APB E005 | |
| Seminar | Research Talk by Isara Anantavrasilp about 'Toward a Formal Model of Sequence Alignment Problem' | DS2, 18. Mai 2015 in APB E005 | |
| Seminar | Report by Sebastian Hahn about 'Modulogame' | DS2, 1. Juni 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, 8. Juni 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, 15. Juni 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, 22. Juni 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, 29. Juni 2015 in APB E005 | |
| Seminar | CANCELD: Talk by Norbert Manthey on "The 'Parallel SAT' Research Project" | DS2, 6. Juli 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, 13. Juli 2015 in APB E2026 | |
| Seminar | Research Talk by Sibylle Möhle on 'Propositional Model Counting and Enumeration' | DS2, 20. Juli 2015 in APB E005 |
Kalender
