Peter Baumgartner in 2003

Peter Baumgartner

Principal Researcher, NICTA
Research Leader/Software Systems Research Group
and ANU CECS

Details and Contact
[ Home | Publications | Activities | Teaching | Student project offers | Systems | Talks ]

Student project offers

Areas of interest

My area is automated deduction (AD). AD is concerned with push-button technology for logical reasoning on computer. AD systems take as input a formula of a formal (mathematical) logical language, such as propositional or first-order predicate logic, and apply inference rules of a logical calculus to analyse the formula for its properties (see here and here for an overview of the area, and here for mathematical logic more in general). Typically, one is interested in determining whether the formula is valid ("always true"), satisfiable ("sometimes true"), under what conditions it is valid, whether it is valid in a fixed interpretation ("model checking"), among others.

Research in AD is highly specialized. My specific research interest is the design of AD systems for first-order predicate logic and applying them to solve real-world problems. I am interested in any application area, such as program development and verification, knowledge representation, in particular ontological reasoning, and, more recently, business rules and process model analysis. See my slides, publications and teaching to get some idea.

Below I describe two research areas that are of interest to me and that are suitable for student projects. Please do not contact me if you are looking for an internship and need financial support for that.

Instance-based methods

Instance-based methods (IBMs) are a family of methods for first-order logic theorem proving. IBMs share the principle of carrying out proof search by maintaining a set of instances of input formulas and analyzing it for satisfiability until completion. IBMs are conceptually essentially different to other, more mainstream, methods like resolution or free-variable analytic tableaux. Also, IBMs exhibit a search space and termination behaviour (in the satisfiable case) different from those methods, which makes them attractive from a practical point of view as a complementary method. For instance, IBMs are decision procedures for function-free clause sets and thus capture the complexity class NEXPTIME. My main interest here is advancing one such IBM, the so-called Model Evolution calculus. A brief overview paper on IBMs is here.

Concrete topics are centered around improving Model Evolution.

Logical analysis of business rules and processes

Business rules (BRs) are declarative statements that describe legal or operational constraints of a business. Business process models (BPMs) descibe execution of workflows. The interest here is to consider automated reasoning techniques to analyze BRs and BPMs, for properties such as consistency, redundancies and certain completeness properties, which helps to make sure that BRs make sense. Another interest is reasoning about BRs and BPMs in combination, in order to support compliance analysis and business process execution planning. We envisage our approach is useful for both offline, static analysis and during runtime, to determine possible next steps as business processes are executed.

For instance, we are looking into transforming BRs and BPMs into first-order logic so that automated theorem provers can be used then. While this is a rather general and powerful approach, it comes with several technical challenges that need to be addressed (termination, scalability, e.g.). Concrete topics will be around these issues.