TY - GEN
T1 - A strong and mechanizable grand logic*
AU - Randall, M.
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2000.
PY - 2000
Y1 - 2000
N2 - The purpose of this paper is to describe a "grand logic", that is, a system of higher order logic capable of use as a general purpose foundation for mathematics. This logic has developed as the logic of a theorem proving system which has had a number of names in its career (EFTTP, Mark2, and currently Watson), and the suitability of this logic for computer-assisted formal proof is an aspect which will be considered, though not thoroughly. A distinguishing feature of this system is its relationship to Quine's set theory NF and related untyped A-calculi studied by the author.
AB - The purpose of this paper is to describe a "grand logic", that is, a system of higher order logic capable of use as a general purpose foundation for mathematics. This logic has developed as the logic of a theorem proving system which has had a number of names in its career (EFTTP, Mark2, and currently Watson), and the suitability of this logic for computer-assisted formal proof is an aspect which will be considered, though not thoroughly. A distinguishing feature of this system is its relationship to Quine's set theory NF and related untyped A-calculi studied by the author.
UR - http://www.scopus.com/inward/record.url?scp=84949195857&partnerID=8YFLogxK
U2 - 10.1007/3-540-44659-1_18
DO - 10.1007/3-540-44659-1_18
M3 - Conference contribution
AN - SCOPUS:84949195857
SN - 9783540678632
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 283
EP - 300
BT - Theorem Proving in Higher Order Logics - 13th International Conference, TPHOLs 2000, Proceedings
A2 - Aagaard, Mark
A2 - Harrison, John
PB - Springer Verlag
T2 - 13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000
Y2 - 14 August 2000 through 18 August 2000
ER -