Knowledge Representation and Reasoning Seminar

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Knowledge Representation and Reasoning Seminar

Lehrveranstaltung mit SWS 0/2/0 (Vorlesung/Übung/Praktikum) in SS 2015

Dozent

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