215:
80:
Automath was never widely publicized at the time, however, and so never achieved widespread use; nonetheless, it proved very influential in the later development of
256:
62:. Propositions were represented as sets (called "categories") of their proofs, and the question of provability became a question of non-emptiness (
171:
150:
129:
249:
59:
285:
242:
92:, a system of writing and checking formalized mathematics that is still in active use, was influenced by Automath.
275:
31:
46:
The
Automath system included many novel notions that were later adopted and/or reinvented in areas such as
34:
starting in 1967, for expressing complete mathematical theories in such a way that an included automated
51:
47:
280:
193:
167:
146:
125:
81:
63:
226:
58:
is one outstanding example. Automath was also the first practical system that exploited the
85:
55:
27:
17:
66:); de Bruijn was unaware of Howard's work, and stated the correspondence independently.
222:
269:
101:
70:
35:
89:
16:
This article is about the programming language. For self-taught individuals, see
69:
L. S. van
Benthem Jutting, as part of this Ph.D. thesis in 1976, translated
214:
166:
Workshop, Dordrecht, Boston, published by Kluwer
Academic Publishers,
199:
187:
196:
homepage of a workshop to celebrate the 35th year of
Automath
230:
141:
R. P. Nederpelt, J. H. Geuvers, R. C. de Vrijer (1994)
145:Vol. 133 of Studies Logic, Elsevier, Amsterdam.
122:Lectures on the Curry–Howard isomorphism
250:
8:
164:Thirty-five years of automating mathematics.
77:into Automath and checked its correctness.
257:
243:
120:Morten Heine Sørensen, Paweł Urzyczyn,
113:
7:
211:
209:
229:. You can help Knowledge (XXG) by
14:
60:Curry–Howard correspondence
213:
26:("automating mathematics") is a
38:can verify their correctness.
1:
194:Thirty Five years of Automath
143:Selected Papers on Automath.
302:
208:
15:
32:Nicolaas Govert de Bruijn
75:Foundations of Analysis
225:-related article is a
162:F. Kamareddine (2003)
52:explicit substitution
48:typed lambda calculus
286:Formal methods stubs
188:The Automath Archive
124:, Elsevier, 2006,
82:logical frameworks
238:
237:
64:type inhabitation
293:
276:Proof assistants
259:
252:
245:
217:
210:
202:by Freek Wiedijk
175:
160:
154:
139:
133:
118:
86:proof assistants
301:
300:
296:
295:
294:
292:
291:
290:
266:
265:
264:
263:
206:
184:
179:
178:
161:
157:
140:
136:
119:
115:
110:
98:
56:Dependent types
44:
28:formal language
21:
18:Autodidacticism
12:
11:
5:
299:
297:
289:
288:
283:
278:
268:
267:
262:
261:
254:
247:
239:
236:
235:
223:formal methods
218:
204:
203:
197:
191:
183:
182:External links
180:
177:
176:
155:
134:
112:
111:
109:
106:
105:
104:
97:
94:
43:
40:
13:
10:
9:
6:
4:
3:
2:
298:
287:
284:
282:
279:
277:
274:
273:
271:
260:
255:
253:
248:
246:
241:
240:
234:
232:
228:
224:
219:
216:
212:
207:
201:
200:Automath page
198:
195:
192:
189:
186:
185:
181:
173:
172:1-4020-1656-5
169:
165:
159:
156:
152:
151:0-444-89822-0
148:
144:
138:
135:
131:
130:0-444-52077-5
127:
123:
117:
114:
107:
103:
102:QED manifesto
100:
99:
95:
93:
91:
87:
83:
78:
76:
72:
71:Edmund Landau
67:
65:
61:
57:
53:
49:
41:
39:
37:
36:proof checker
33:
30:, devised by
29:
25:
19:
231:expanding it
220:
205:
163:
158:
142:
137:
121:
116:
90:Mizar system
79:
74:
68:
45:
23:
22:
281:Type theory
270:Categories
132:, pp 98-99
108:References
190:(mirror)
96:See also
42:Overview
24:Automath
170:
149:
128:
88:. The
221:This
227:stub
168:ISBN
147:ISBN
126:ISBN
84:and
50:and
73:'s
272::
54:.
258:e
251:t
244:v
233:.
174:.
153:.
20:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
