PROOFS IN HIGHER ORDER LOGIC

Description

Niveau: Supérieur

• dissertation

eq PROOFS IN HIGHER-ORDER LOGIC Dale A. Miller October 1983 Tech Report: MS-CIS-83-37 This dissertation was submitted to the Mathematics Department of Carnegie-Mellon University on 27 August 1983 in partial fulfillment of the requirements for the degree of Doctor of Philosophy. In October 1983 it was released as Tech Report MS-CIS-83-37 from the Computer Science and Information Department at the University of Pennsylvania. The current version is the result of recompiling the original TeX source files (not LaTeX files) in August 2004. In the process, three figures have not been reproduced (they are not particularly important for the text). This work was supported by NSF grant MCS81-02870.

• provers can


• skolem functions


• herbrand instances


• expansions trees


• higher-order logic


• order theorem

Sujets

• Dissertation
• Andrews
• Higher-order logic

Informations

• Publié par: profil-nechor-2012
• Nombre de lectures: 9
• Langue: English

Extrait

eq

PROOFS IN HIGHER-ORDER LOGIC

Dale A. Miller October 1983 Tech Report: MS-CIS-83-37

This dissertation was submitted to the Mathematics Department of Carnegie-Mellon University on 27 August 1983 in partial fulllment of the requirements for the degree of Doctor of Philosophy. In October 1983 it was released as Tech Report MS-CIS-83-37 from the Computer Science and Information Department at the University of Pennsylvania. The current version is the result of recompiling the original TeX source les (not LaTeX les) in August 2004. In the process, three gures have not been reproduced (they are not particularly important for the text).

This work was supported by NSF grant MCS81-02870.

1: Introduction and Summary

2.1: The Logical SystemT

2.2: Abstract Derivability Property

2.2: Abstract Derivability Property

2.3: Expansion Tree Proofs