Automated Reasoning Tools

at the

University of Miami

The Automated Reasoning Tools (ARTists) research group, in the Department of Computer Science at the University of Miami, is investigating and building software systems that have Automated Reasoning (AR) components. Areas of interest include:

Evaluation and certification of Automated Theorem Proving (ATP) systems, including:
- The TPTP problem library
- The TSTP solution library
Usable interfaces to AR systems - the PMT project, including:
- Steven's IDV interactive derivation viewer. Watch the video.
- Geoff's (previously Diego's, and before that Seyyed's) GDV semantic derivation verifier
- Yi's, and now Yury's, AGInT for Automatic Generation of INteresting Theorems
- Yury's Prophet syntactic relevancy measurer, and YuCS axiom combination selector
- The System before TPTP, System on TPTP, and System on TSTP online services.
ATP systems:
- SRASS, Faust Ratify, RedAx, GrAnDe, CSSCPA
Systems for formalized mathematics, including:
- Techniques for Rich Theories (RTs)
- Reverse Decimal Notation (RDN) Arithmetic in first order logic

Group Members:

Photos:

The ARTists, Spring 2008
MLAR display at RCF 2008
The ARTists, Spring 2007
The ARTists, Fall 2006
The ARTists' Seattle Reunion, Summer 2006
The ARTists, Spring 2006
The ARTists, Spring 2005
The ARTists, Fall 2003
Faust display at RCF 2004 (Close up)

Ex-members:

Anna Bystrik
Diego Belfiore (DVDV, May 2005)
Seyyed Dashti (worked on DV, did not write thesis)
Sasha Dvorsky (provided Mathematical examples)
Yi Gao (AGInT, Summer 2004)
Gonzalo Martinez (ATPResults, Spring 2007)
Michael Metral (Sigma, Fall 2006)
Yury Puzis (AGInT, Prophet, Faust, 2004-2007)
Weina Shen (Modal Logic, Fall 2006)
Jason Wester (CSSCPA, May 2005)
Yingxin Xing (YxY interface, Fall 2003)
Yuan Zhang (YuLM+, Summer 2005)
Patrick Zhou (worked on PMT, moved out of town)