`Travelled to:`

1 × France

1 × Germany

3 × USA

`Collaborated with:`

∅ C.E.Brown M.Bishop S.Issar F.Pfenning D.Miller E.L.Cohen D.Nesmith D.Nesmith C.P.Klapper

`Talks about:`

tps (6) theorem (5) system (5) prove (5) higher (2) order (2) logic (2) transform (1) instanti (1) descript (1)

## Person: Peter B. Andrews

### DBLP: Andrews:Peter_B=

### Contributed to:

### Wrote 9 papers:

- CADE-2000-AndrewsB #education #higher-order #logic #named #proving #theorem proving #tutorial #using
- Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic (PBA, CEB), pp. 511–512.
- CADE-2000-AndrewsBB #proving #theorem proving #type system
- System Description: TPS: A Theorem Proving System for Type Theory (PBA, MB, CEB), pp. 164–169.
- CADE-1998-BishopA
- Selectively Instantiating Definitions (MB, PBA), pp. 365–380.
- CADE-1990-AndrewsINP #proving #theorem proving
- The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 641–642.
- CADE-1988-AndrewsINP #proving #theorem proving
- The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 760–761.
- CADE-1986-Andrews #higher-order #logic
- Connections and Higher-Order Logic (PBA), pp. 1–4.
- CADE-1986-AndrewsPIK #proving #theorem proving
- The TPS Theorem Proving System (PBA, FP, SI, CPK), pp. 663–664.
- CADE-1982-MillerCA
- A Look at TPS (DM, ELC, PBA), pp. 50–69.
- CADE-1980-Andrews #deduction #proving
- Transforming Matings into Natural Deduction Proofs (PBA), pp. 281–292.