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