369:
124:
is based on the resolution rule to solve literals and narrowing to evaluate functional expressions. To reduce the number of possible narrowing steps, a leftmost-innermost basic narrowing strategy is used which, it is claimed, can be efficiently implemented. Terms are simplified by rewriting before a
125:
narrowing step is applied and equations are rejected if the two sides have different constructors at the top. Rewriting and rejection are supposed to result in a large reduction of the search tree and produce an operational semantics that is more efficient than
162:
Repository, ALF is included as an AI programming language, more so as a functional/logic programming language Prolog implementation. A user manual describing the language and the use of the system is available. The ALF System runs on
119:
ALF was designed to be genuine integration of both programming paradigms, and thus any functional expression can be used in a goal literal and arbitrary predicates can occur in conditions of equations. ALF's
148:(WAM) with several extensions to implement narrowing and rewriting. In the current ALF implementation programs of this abstract machine are executed by an emulator written in
232:
439:
136:
The ALF system was designed to be an efficient implementation of the combination of resolution, narrowing, rewriting, and rejection. ALF programs are
199:
116:
logic with equality, which consists of predicates and Horn clauses for logic programming, and functions and equations for functional programming.
429:
265:
324:
294:
410:
220:
434:
384:
41:
174:
that grants the right to use for "evaluation, research and teaching purposes" but not commercial or military use.
444:
403:
191:
228:
195:
156:
149:
159:
145:
129:'s resolution strategy. Similarly to Prolog, ALF uses a backtracking strategy corresponding to a
396:
254:
105:
49:
316:
121:
354:
168:
101:
36:
17:
8:
290:
261:
130:
109:
45:
60:
376:
171:
141:
348:
380:
423:
113:
323:. Institut für Informatik, Christian-Albrechts-Universität zu Kiel.
293:. Institut für Informatik, Christian-Albrechts-Universität zu Kiel.
137:
351:, including many articles relevant to the design and theory of ALF
368:
126:
85:
164:
24:
355:
Information about getting and installing the ALF system
221:"ALF: Algebraic Logic Functional programming language"
252:
23:For the action language for foundational UML, see
421:
404:
253:Hanus, Michael; Andreas Schwab (1995-02-13).
440:Programming languages created in the 1990s
411:
397:
192:"CMU Artificial Intelligence Repository"
262:Christian-Albrechts-Universität zu Kiel
430:Functional logic programming languages
422:
225:CMU Artificial Intelligence Repository
282:
213:
184:
363:
327:from the original on 2 December 2015
246:
13:
14:
456:
342:
314:
297:from the original on 25 June 2007
288:
271:from the original on 11 July 2007
202:from the original on 23 June 2007
367:
235:from the original on 10 May 2007
167:and is available under a custom
308:
112:techniques. Its foundation is
1:
349:Publications of Michael Hanus
177:
16:For the proof assistant, see
383:. You can help Knowledge by
7:
260:. Institut für Informatik,
10:
461:
435:Compilers and interpreters
362:
229:Carnegie Mellon University
196:Carnegie Mellon University
157:Carnegie Mellon University
94:Algebraic Logic Functional
22:
15:
84:
79:
55:
35:
144:, which is based on the
140:into instructions of an
133:in the derivation tree.
317:"ALF License Agreement"
160:Artificial Intelligence
146:Warren Abstract Machine
445:Computer science stubs
122:operational semantics
169:proprietary software
102:programming language
18:ALF (theorem prover)
255:"ALF User's Manual"
32:
131:depth-first search
30:
392:
391:
110:logic programming
91:
90:
452:
413:
406:
399:
377:computer science
371:
364:
336:
335:
333:
332:
315:Hanus, Michael.
312:
306:
305:
303:
302:
291:"The ALF System"
289:Hanus, Michael.
286:
280:
279:
277:
276:
270:
259:
250:
244:
243:
241:
240:
217:
211:
210:
208:
207:
188:
142:abstract machine
75:
72:
70:
68:
66:
64:
62:
33:
29:
460:
459:
455:
454:
453:
451:
450:
449:
420:
419:
418:
417:
360:
345:
340:
339:
330:
328:
313:
309:
300:
298:
287:
283:
274:
272:
268:
257:
251:
247:
238:
236:
219:
218:
214:
205:
203:
190:
189:
185:
180:
59:
28:
21:
12:
11:
5:
458:
448:
447:
442:
437:
432:
416:
415:
408:
401:
393:
390:
389:
372:
358:
357:
352:
344:
343:External links
341:
338:
337:
321:The ALF System
307:
281:
245:
231:. 1995-02-13.
212:
198:. 1995-02-13.
182:
181:
179:
176:
89:
88:
82:
81:
77:
76:
57:
53:
52:
42:multi-paradigm
39:
9:
6:
4:
3:
2:
457:
446:
443:
441:
438:
436:
433:
431:
428:
427:
425:
414:
409:
407:
402:
400:
395:
394:
388:
386:
382:
379:article is a
378:
373:
370:
366:
365:
361:
356:
353:
350:
347:
346:
326:
322:
318:
311:
296:
292:
285:
267:
263:
256:
249:
234:
230:
226:
222:
216:
201:
197:
193:
187:
183:
175:
173:
170:
166:
161:
158:
153:
151:
147:
143:
139:
134:
132:
128:
123:
117:
115:
111:
107:
103:
99:
95:
87:
83:
80:Influenced by
78:
74:
58:
54:
51:
47:
43:
40:
38:
34:
26:
19:
385:expanding it
374:
359:
329:. Retrieved
320:
310:
299:. Retrieved
284:
273:. Retrieved
248:
237:. Retrieved
224:
215:
204:. Retrieved
186:
154:
135:
118:
97:
93:
92:
114:Horn clause
63:.informatik
424:Categories
331:2020-03-06
301:2007-06-22
275:2007-06-22
239:2007-06-22
206:2007-06-22
178:References
106:functional
50:functional
104:combines
65:.uni-kiel
325:Archived
295:Archived
266:Archived
233:Archived
200:Archived
138:compiled
71:/systems
37:Paradigm
172:license
155:In the
56:Website
127:Prolog
86:Prolog
375:This
269:(PDF)
258:(PDF)
46:logic
381:stub
165:Unix
108:and
73:/ALF
69:/~mh
25:FUML
98:ALF
67:.de
61:www
31:ALF
426::
319:.
264:.
227:.
223:.
194:.
152:.
100:)
48:,
44::
412:e
405:t
398:v
387:.
334:.
304:.
278:.
242:.
209:.
150:C
96:(
27:.
20:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.