Principal Research Scientist, Data61
Details and Contact
- Possible models computation and revision by shallow embedding into Scala.
- SMTtoTPTP - A translator from SMT-LIB to TPTP TFF.
- BEAGLE - a theorem prover for
- 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
year at the major conference
CADE/IJCAR (International Conference on
Automated Reasoning) in the field. The theorem prover
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
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).
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.
- KRHyper extended with equality reasoning and many more features; formerly known as E-KRHyper.