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 Alex's Aprils latent semantics relevancy measurer.
- Aparna's Multiple Answer Extrator system (rudely renamed from "tellMe" when reimplemented by Geoff - don't blame Aparna).
- The System before TPTP, System on TPTP, and System on TSTP online services.
ATP systems:
- SPASS-XDB, Divvy, SRASS, Ratify, RedAx, GrAnDe, CSSCPA

Group Members:

Nelson Dellis
Jose Hernandez
Michael Schick
Alexandra (Alex) Teyssandier
Geoff Sutcliffe

Photos:

The ARTists, Spring 2010
The ARTists, Fall 2009
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 (Main projects, time of exit):

Anna Bystrik (2003)
Diego Belfiore (DVDV, May 2005)
Seyyed Dashti (worked on DV, did not write thesis, 2002)
Sasha Dvorsky (provided Mathematical examples, 2003)
Yi Gao (AGInT, Summer 2004)
Aman Kakkad (MLAR, 2009)
Gonzalo Martinez (ATPResults, Spring 2007)
Michael Metral (Sigma, Fall 2006)
Yury Puzis (AGInT, Prophet, Faust, 2004-2007)
Alex Roederer (APRILS, 2009)
Weina Shen (Modal Logic, Fall 2006)
Steven Trac (IDV and Sigma and ..., 2008)
Josef Urban (MaLARea, 2008)
Jason Wester (CSSCPA, May 2005)
Yingxin Xing (YxY interface, Fall 2003)
Aparna Yerikalapudi (tellMe, 2008)
Yuan Zhang (YuLM+, Summer 2005)
Patrick Zhou (worked on PMT, moved out of town, 2002)