Peter Baumgartner

Student research projects

In the following I describe possible topics for students interested in working with me. This can be towards a honors degree, a masters degreee or a Ph.D. degree. Concrete projects for Summer Research Scholar Projects are listed also on this page, see Logic and Computation there.

Area: Automated Deduction. My working area is automated deduction (AD). In case you never heard of it, AD is concerned with, roughly, the design of push-button technology that enables computers to reason logically. AD systems do that by (typically) taking as input some formulas (of a certain formal logical language, such as predicate logic), analyzing them by application of logical inference rules, and delivering the result (such as: "yes, I found a proof of your conjecture").

What's the relevance? Formal logical languages provide a mathematical foundation for many areas of computer science. They are used as specification languages within, e.g., program development and verification, hardware design and verification, relational databases, and many subfields of Artificial Intelligence, such as planning and knowledge representation (e.g. the Semantic Web). Now, AD provides algorithms and implemented systems for solving problems in these areas. (Originally, AD was motivated by the desire to automatically prove mathematical theorems, which still applies to a certain degree today.)

Specific interest. AD as a field is much to broad for a single researcher to cover all of it. My main interest is in developing AD systems for classical first-order logic and their applications. (But I am also interested in related disciplines, such as logic programming.) If you want to find out more please have a look at my slides, publications or teaching below. If you find something interesting for you, and if you would like to work with me, please let me know by Email or just drop in!

Logical Analysis of Business Rules.

Business Rules are widely used in industry to specify the conditions or constraints that control the operations of a business. For instance, business rules might reflect legislation governing visa regulations, or conditions under which social benefits are granted.

The background of this project is a running project between NICTA and a Canberra-based SME. We are building a prototype system that allows to analyze sets of business rules for logical errors, such as inconsistencies and functional dependencies. Spotting such errors is of great importance in the development phase of business rules. The goal is to help with extending our already existing prototype by enhancing its functionality (both the user front-end and the internal reasoning engine).

Requirements. Good Java programming skills. Some background in mathematical logic and/or constraint processing would be useful.

Student's gain.

• Becoming acquainted with business rules and automated reasoning techniques
• Involvement in leading-edge applied research in the intersection of these areas
• Honours project or Ph.D. project

Instance-Based Methods.

Being relatively new, there are lots of interesting open issues, both theoretically and practically that could be explored in honors or Ph.D. projects.

Some specific suggested topics. The practical ones are about extending the Darwin theorem prover, one of the leading systems of its kind, which is (co-)developed in our group.

• Equality reasoning: reasoning with equations is of paramount importance in virtually all application areas. As the theory of doing this within Darwin is already developed (one could always improve, though) this is mostly a programming project. Programming language is OCaml.
• Numbers: first-order theorem provers are utterly bad with numbers. This project is about adding and experimenting with finite-domain integer arithmetic to Darwin. This could be done by clever encoding arithmetic in the input and/or extending Darwin.
• Minimal model computation: Darwin can compute finite models of first-order logic formulas (provided they exist). For some applications, e.g., within computational linguistics or diagnosis, it is not enough to deliver just any model. One wants to have a minimal model. In diagnosis, for instance, this corresponds to the experience that usually only a minimal set of components of a device breaks at a time.
• Some domains are necessarily infinite, e.g., the integers. Instance-based methods are bad at detecting satisfiability in presence of axiom sets that admit infinite models only. Can we find a clever mechanism to improve the situation, i.e. to discover and represent (certain) infinite models? This is a challenging (also) theoretical project.
• Many practically interesting problem classes are NEXPTIME-complete (complete for nondeterministic exponential time), like for instance satisfiability of SHOIQ knowledge bases (SHOIQ is a very important logical language used for the Semantic Web), first-order model expansion (a certain kind of constraint satisfaction problems), satisfiability of formulas of the so-called Ackermann-Class with equality, Satisfiability of DQBF (Dependancy Quantified Boolean Formulas), First-Order logic with two variables and counting quantifiers ... Other interesting applications are quantified constraint satisfaction problems (QCSPs) over finite domains, in particular QBF (quantified boolean formulas).

  Now, Instance-Based Methods are decision procedures for so-called function-free clause logic, the satisfiability problem of which is exactly NEXPTIME! Thus, there are efficient (polynomial) transformation from the mentioned problems into function-free clause logic. This suggests to investigate this path from a practical point of view, i.e. to look at existing transformations, check if they are feasible, perhaps improve them and try an instance-based method, e.g. the Darwin prover, on some problems.

Logic Summer School, Canberra, January 2009

• Slides (PDF)
• Example problems discussed in the lectures, and some more (see the files for more information):
  • Three-coloring problem instance
  • Three-coloring problem - (dis)prove of functional dependency
  • Disprove "all groups are abelian"
  • A pigeon-hole problem, usable with otter, SOS strategy
  • A pigeon-hole problem, usable with otter, auto-mode
• Theorem provers:
  • Otter (caution: otter does not accept .p files)
  • Darwin - A Theorem Prover for the Model Evolution Calculus
  • Paradox - A First-Order Logic Model Finder

WS 2004/2005

SS 2004

WS 2003/2004

WS 2002

SS 2002

WS 2001/2002

SS 2001

• Informatik II.
  "Introduction to Computer Science"
  Introductory level course to be given in the summer term 2001 at the University of Giessen (in German).
• Projektarbeiten im Fortgeschrittenen-Praktikum Informatik
  (Universität Giessen)

WS 2000/2001

• Einführung in die Informatik für IM I.
  "Introduction to Computer Science for Information Managers".
  Introductory level course given in the winter term 2000/2001 at the University of Koblenz (in German).
• Informatik III.
  "Introduction to Computer Science."
  Introductory level course given in the winter term 2000/2001 at the University of Giessen (in German).

SS 2000 and before

• Verifikation Verteilter Systeme.
  "Verification of distributed systems." Graguate-level course given in the summer term 2000 at the University of Koblenz (in German).
• Software Verification.
  Graguate-level course given in the fall term 1998 at the University of New Brunswick, Frederiction, New Brunswick, Canada.

Material on other lectures I gave on logic and/or knowledge representation are available on request.