Entry Paulson:1985:LLL from compj1980.bib
Last update: Sat Jan 6 02:03:49 MST 2018
Top |
Symbols |
Math |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z
BibTeX entry
@Article{Paulson:1985:LLL,
author = "Lawrence C. Paulson",
title = "Lessons Learned from {LCF}: a Survey of Natural
Deduction Proofs",
journal = j-COMP-J,
volume = "28",
number = "5",
pages = "474--479",
month = nov,
year = "1985",
CODEN = "CMPJA6",
DOI = "https://doi.org/10.1093/comjnl/28.5.474",
ISSN = "0010-4620 (print), 1460-2067 (electronic)",
ISSN-L = "0010-4620",
bibdate = "Tue Dec 4 14:48:19 MST 2012",
bibsource = "Compendex database;
http://comjnl.oxfordjournals.org/content/28/5.toc;
http://www.math.utah.edu/pub/tex/bib/compj1980.bib;
http://www3.oup.co.uk/computer_journal/hdb/Volume_28/Issue_05/",
URL = "http://comjnl.oxfordjournals.org/content/28/5/474.full.pdf+html;
http://www3.oup.co.uk/computer_journal/hdb/Volume_28/Issue_05/tiff/474.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_28/Issue_05/tiff/475.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_28/Issue_05/tiff/476.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_28/Issue_05/tiff/477.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_28/Issue_05/tiff/478.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_28/Issue_05/tiff/479.tif",
acknowledgement = ack-nhfb,
affiliation = "Computer Lab, Cambridge, Engl",
affiliationaddress = "Computer Lab, Cambridge, Engl",
classcodes = "C4210 (Formal logic)",
classification = "723",
corpsource = "Comput. Lab., Cambridge, UK",
fjournal = "The Computer Journal",
journal-URL = "http://comjnl.oxfordjournals.org/",
keywords = "backwards proof; computer metatheory; computer
programming languages; computer software; formal logic;
interactive proof assistants; LCF project; LCF system;
logic PPLAMBDA; metalanguage MI; natural deduction
proofs; rewriting; theorem proving; theorem-provers",
treatment = "T Theoretical or Mathematical",
}
Related entries
- backward,
25(1)93,
28(5)466
- deduction,
31(2)125
- formal,
27(2)121,
28(1)59,
28(2)112,
28(2)162,
28(5)480,
29(6)481,
30(2)134,
30(2)183,
30(4)316,
30(4)328,
30(4)337,
30(6)507,
31(4)313,
31(4)325,
31(4)336,
31(6)510,
31(6)525,
31(6)564,
32(1)1,
32(1)36,
32(1)90,
32(1)91,
32(4)290,
32(4)305,
32(4)351,
32(5)385,
32(5)399,
32(5)413,
32(5)422,
32(5)432,
32(5)445
- interactive,
23(3)233,
24(1)62,
24(2)191,
25(3)399,
26(1)93,
26(2)187,
26(3)199,
26(3)235,
27(1)8,
27(2)112,
28(1)22,
28(2)117,
29(1)38,
29(2)176,
29(3)201,
29(5)385,
29(5)396,
31(5)445,
31(5)457,
32(1)21,
32(1)86,
32(2)142,
32(2)162,
32(6)516
- Lessons,
26(2)154,
32(6)533
- logic,
23(2)165,
23(2)191,
25(1)140,
25(2)218,
25(2)287,
27(3)260,
28(2)112,
28(5)487,
29(1)9,
29(1)12,
29(1)17,
29(3)241,
29(3)246,
29(6)481,
29(6)495,
29(6)545,
30(1)77,
30(2)134,
30(2)183,
30(3)258,
30(3)283,
30(5)386,
30(5)393,
31(2)133,
31(3)220,
31(4)336,
31(6)510,
31(6)525,
31(6)564,
32(1)29,
32(1)36,
32(1)90,
32(1)91,
32(4)290,
32(5)399,
32(5)445,
32(5)453
- metalanguage,
26(2)164
- metatheory,
23(1)34,
23(3)243,
27(4)376,
28(1)9,
28(3)195,
28(3)250,
28(3)257,
28(5)487,
29(1)24,
29(1)76,
29(2)103,
29(2)161,
29(2)187,
29(5)404,
29(6)481,
29(6)531,
29(6)538,
29(6)545,
30(1)8,
30(1)27,
30(1)43,
30(2)134,
30(3)223,
30(4)376,
30(4)378,
30(6)507,
31(4)325,
31(4)336,
31(6)510,
32(1)93
- natural,
23(1)3,
23(1)22,
29(5)460,
31(6)550,
32(2)108
- project,
26(3)247,
28(3)291,
29(2)151,
29(3)201,
29(3)246,
29(6)527,
30(1)63,
30(5)469,
31(5)391,
32(2)152,
32(5)386
- proof,
27(3)230,
29(1)17,
29(5)404,
29(6)531,
30(4)376,
30(6)507,
31(4)289,
32(2)122
- provers, theorem-,
31(6)510
- proving,
27(3)230,
28(2)105,
31(1)51,
31(6)510,
32(5)437
- rewriting,
29(2)171
- survey,
23(4)377,
24(2)139,
25(1)130,
26(4)354,
28(1)82,
30(3)233,
32(2)175
- theorem,
27(1)8,
27(3)230,
28(2)105,
29(3)277,
31(1)17,
31(1)51,
31(6)510,
32(5)437
- theorem-provers,
31(6)510