## Peter Baumgartner

Principal Research Scientist, Data61

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. Often this requires "smarter"
theorem provers than those available today, by adding dedicated reasoning support for
specific theories, such as (integer) arithmetic.

Please see the
Automated
Reasoning
project page for more information on what we are doing.

I welcome students to work with me on in the areas mentioned. Student
projects can be carried out towards a
honors degree, a masters degreee, a
Ph.D. degree, a Summer Internship or a project in the Erasmus Mundus
CL program. We have compiled a list of
projects that is
targetted for EMCL students but other students may find something of interest
as well.

General information on NICTA scholarships is
here.