Peter Baumgartner

Talks

Tutorials

• Instance Based Methods.
  Tutorial held together with Gernot Stenz at TABLEAUX 2005 (Automated Reasoning with Analytic Tableaux and Related Methods), Koblenz, Germany, 2005. [ Handout (PDF) | Slides (PDF) ]
• Automated Deduction for Computational Semanticists.
  Slides of "Part II - Bottom-Up Computation and Model Generation", tutorial held at ICoS-3 (Inference in Computational Semantics), Siena, Italy, June 2001.
• Clause Normalform Tableaux.
  Tutorial held at CADE 15 (15th Conference on Automated Deduction), Lindau, Germany.

• First-Order Theorem Proving [ Slides (PDF) | Handout (PDF) ]
  The handout has the same contents as the slides, but 4 slides per page
• Example problems discussed in the lecture (see the files for how to use them):
  • Three-coloring problem instance
  • Three-coloring problem - (dis)prove of functional dependency
  • Disprove "all groups are abelian"
  • A SUDOKU instance
• Theorem provers used for the above problems:
  • Darwin - A Theorem Prover for the Model Evolution Calculus
  • Paradox - A First-Order Logic Model Finder

Invited Conference Talks

• Logical Engineering with Instance-Based Methods.
  CADE-21 (Bremen, Germany, July, 2007).
• A First-Order Davis-Putnam-Loveland-Logeman Procedure.
  'Distinguished paper track' at IJCAI 2001 (Seattle, USA, August, 2001).

Selected Technical Talks

• Theories in Context - Model Evolution Modulo Integer Constraints [ PDF ].
  Dagstuhl Seminar on Deduction and Decision Procedures, Germany, September, 2007.
• Lemma Learning in the Model Evolution Calculus [ PDF ].
  LPAR 2006, Phnom Penh, Cambodia, November 2006.
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods [ PDF ].
  IJCAR 2006, Seattle, USA, August 2006.
• The Model Evolution Calculus with Equality [ Powerpoint (requires TeX4PPT extension to Powerpoint) | PDF ].
  CADE-20, Tallin, Estland, July 2005.
• The Model Evolution Calculus and an Application to Ontological Reasoning [ Powerpoint (requires TeX4PPT extension to Powerpoint) | PDF ].
  The University of Birmingham, June 2005.
• Automated Deduction Techniques for Knowledge Representation Applications [ Powerpoint (requires TeX4PPT extension to Powerpoint) | PDF ].
  Currently evolving ideas for using first-order provers for ontological reasoning.
• The Model Evolution Calculus with Built-in Theories [ Powerpoint (requires TeX4PPT extension to Powerpoint) | PDF ].
  AG-2 group meeting, Saarbrücken, Germany, October 2004.
• The Bernays-Schönfinkel Fragment of First-Order Autoepistemic Logic [ Powerpoint (requires TeXPoint extension to Powerpoint) | Slides in PNG Format ].
  Deduktionstreffen, Saarbrücken, Germany, October 2004.
• Logic Programming Infrastructure for Inferences on FrameNet. [ Powerpoint | PDF ], also presented: Picture1, Picture2.
  Informatik Kolloquium TU Clausthal-Zellerfeld, Germany, July 2004.
  
• Splitting an operator - An algebraic modularity result and its application to logic programming.
  Slides of a talk held at an internal meeting at AG2, Max-Planck-Institut for Computer Science, April 2004.
• Path-Based Query Computation by Automated Deduction.
  Slides of talk held at an internal meeting at AG5, Max-Planck-Institut for Computer Science, January 2004.
• Autoepistemic Logic, Description Logics and Logic Programming [ GIF files | Powerpoint Viewer | Windows Web Archive ].
  Slides of talk held at the "Forschungsseminar Computerlinguistik", Universität des Saarlandes, January 2004.
  Somewhat Obsolete. Please see talk on The Bernays-Schönfinkel Fragment of First-Order Autoepistemic Logic above.
• The Model Evolution Calculus [ Powerpoint | PDF ].
  Colloquium talk at the Chalmers University Gothenburg, Sweden, November 2003.
• Model-Based Deduction for Knowledge Representation.
  Slides of a talk held at the 17. Workshop on Logic Programming, Dresden, December 2002.
• A "Living Book".
  Talk held at the MMISS Workshop (MultiMedia Instruction in Safe Systems), Frauenchiemsee, Germany, October 2002.
• Computing Well-Founded Models on the First-Order Level.
  Slides of a talk held at the annual meeting of the GI special interest group "Deduction Systems", Freiburg, Germany, October 2002.
• Deductive Knowledge Management for Personalized Documents.
  Slides of a talk held 'in-house'. A less technical version of the talk listed next. It also contains more recent ideas. Koblenz, September 2001.
• Deductive Knowledge Management for Personalized Documents.
  Slides of a talk held at the 'Teleseminar Koblenz/Karlsruhe' (Koblenz), December 2000.
• A Confluent Connection Calculus.
  Slides of a talk held at the international workshop 'Deduction', Dagstuhl, Germany, March 1999, and held at the conference on 'Automated Deduction - CADE-16, July 1999.
• Tableaux with Generalized Merges.
  Slides of a talk held at the APICS Computer Science Conference, Saint Mary's University, Halifax, Nova Scotia, Canada, October, 1998.
• Software Verification: Saving user interactions by automated theorem proving.
  Some of the slides of a talk held at the Colloquium of the Faculty of Computer Science, University of New Brunswick, Fredericton, New Brunswick, Canada, October 1998.

  More technical slides (Tools 98, Malente) describe the coupling of the KIV Software verification system with the PROTEIN theorem prover.

• The P(x) v Q(x) Problem.
  Slides of a talk held at the Colloquium of the Institute for Computer Science, University of Munich, July 1998.
• Theory Reasoning in Connection Calculi and the Linearizing Completion Approach.
  Slides of my thesis defense talk (in German).
• A Predicative Transformation for Equality.
  Slides of a talk given at the Meeting of the Implementation Group within the DFG Schwerpunkt 'Deduktion' (Koblenz, Dez. 95).
  The paper is not yet written :-(