Peter B. Andrews - researchr alias

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 31 from 31

2006

TPS: A hybrid automatic-interactive system for developing proofsPeter B. Andrews, Chad E. Brown. japll, 4(4):367-395, 2006. [doi]

2005

Proving Theorems of Type Theory Automatically with TPSPeter B. Andrews. AAAI 2005: 1676-1677

Some Reflections on Proof TransformationsPeter B. Andrews. BIRTHDAY 2005: 14-29 [doi]

2004

ETPS: A System to Help Students Write Formal ProofsPeter B. Andrews, Chad E. Brown, Frank Pfenning, Matthew Bishop, Sunil Issar, Hongwei Xi. JAR, 32(1):75-92, 2004. [doi]

2003

Herbrand Award Acceptance SpeechPeter B. Andrews. JAR, 31(2):169-187, 2003. [doi]

2001

Classical Type TheoryPeter B. Andrews. In John Alan Robinson, Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes). pages 965-1007, Elsevier and MIT Press, 2001.

2000

Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching LogicPeter B. Andrews, Chad E. Brown. cade 2000: 511-512

System Description: TPS: A Theorem Proving System for Type TheoryPeter B. Andrews, Matthew Bishop, Chad E. Brown. cade 2000: 164-169

1998

Selectively Instantiating DefinitionsMatthew Bishop, Peter B. Andrews. cade 1998: 365-380 [doi]

1996

On Sets, Types, Fixed Points, and CheckerboardsPeter B. Andrews, Matthew Bishop. tableaux 1996: 1-15

TPS: A Theorem-Proving System for Classical Type TheoryPeter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi. JAR, 16(3):321-353, 1996.

1993

TPS: An Interactive and Automatic Tool for Proving Theorems of Type TheoryPeter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi. tphol 1994: 366-370

1991

More on the Problem of Finding a Mapping between Clause Representation and Natural Deduction RepresentationPeter B. Andrews. JAR, 7(2):285-286, 1991.

1990

The TPS Theorem Proving SystemPeter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning. cade 1990: 641-642

1989

On Connections and Higher-Order LogicPeter B. Andrews. JAR, 5(3):257-291, 1989.

1988

The TPS Theorem Proving SystemPeter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning. cade 1988: 760-761

1986

Connections and Higher-Order LogicPeter B. Andrews. cade 1986: 1-4

An introduction to mathematical logic and type theory - to truth through proofPeter B. Andrews. Computer science and applied mathematics, Academic Press, 1986.

The TPS Theorem Proving SystemPeter B. Andrews, Frank Pfenning, Sunil Issar, C. P. Klapper. cade 1986: 663-664

1982

A Look at TPSDale Miller, Eve Longini Cohen, Peter B. Andrews. cade 1982: 50-69

1981

Theorem Proving via General MappingsPeter B. Andrews. JACM, 28(2):193-214, 1981. [doi]

1980

Transforming Matings into Natural Deduction ProofsPeter B. Andrews. cade 1980: 281-292

1977

Theorem Proving in Type TheoryPeter B. Andrews, Eve Longini Cohen. IJCAI 1977: 566-566

1976

Refutations by MatingsPeter B. Andrews. TC, 25(8):801-807, 1976.

1974

Resolution and the consistency of analysisPeter B. Andrews. ndjfl, 15(1):73-84, 1974. [doi]

1972

General Models, Descriptions, and Choice in Type TheoryPeter B. Andrews. JSYML, 37(2):385-394, 1972.

General Models and ExtensionalityPeter B. Andrews. JSYML, 37(2):395-397, 1972.

1971

Resolution in Type TheoryPeter B. Andrews. JSYML, 36(3):414-432, 1971.

1968

Resolution With MergingPeter B. Andrews. JACM, 15(3):367-381, 1968. [doi]

A Correction Concerning ResolutionPeter B. Andrews. JACM, 15(4):720, 1968. [doi]

On Simplifying the Matrix of a WFFPeter B. Andrews. JSYML, 33(2):180-192, 1968.

Sign in or sign up to see more results.

runs on WebDSL