Peter Baumgartner

Systems

• Fusemate - Possible models computation and revision by shallow embedding into Scala.
• SMTtoTPTP - A translator from SMT-LIB to TPTP TFF.
• BEAGLE - a theorem prover for hierarchic superposition.
• Fitzroy - a CTL*(FO) model checker.
• Darwin - A Theorem Prover for the Model Evolution Calculus.
• E-Darwin - Darwin with built-in inference rules for equality.
• Yarralumla - Yet Another Range Restriction, Avoiding Loops Under Much Less Assumptions.

The automated theorem proving systems competition CASC is held each year at the major conference CADE/IJCAR (International Conference on Automated Reasoning) in the field. The theorem prover Darwin, jointly developed at the University of Iowa, USA (Alexander Fuchs, Cesare Tinelli) and NICTA's Logic and Computation program (Peter Baumgartner, Canberra) participated at this years competition during IJCAR 2006 in Seattle, USA.

Darwin was entered in four categories. It won the so-called EPR category (function-free clause logic, which is relevant, for instance, in database contexts) and scored third in the SAT category (satisfiable first-order logic formulas).

In the 2007 edition of CASC, Darwin won the EPR category again and scored third in the SAT and FNT categories.

• KRHyper - A first order logic theorem proving and model generation system based on the hyper tableau calculus.
• Hyper - KRHyper extended with equality reasoning and many more features; formerly known as E-KRHyper.