| Zeit und Ort: |
Di 8:30 - 10:00, Raum MW 0350 |
| Beginn: |
19.4.2005 |
| Übungsleitung: |
Stefan
Berghofer |
Einteilung der Praktikumsgruppen
| Studenten | Betreuer |
| Simon Funke, Johannes Hölzl, Florian Zuleger | Markus Wenzel |
| Lukas Bulwahn, Bernhard Häupler, Alexander Sporn | Stefan Berghofer |
| Victor Grajdeanu, Thomas Nitsche, Michael Vögele | Tobias Nipkow |
Hinweise zu Isabelle
Hinweise zu ML
- Der PolyML Compiler kann auf den Suns in der Rechnerhalle mit
<POLYML-HOME>/poly <POLYML-HOME>/ML_dbase
gestartet werden, wobei <POLYML-HOME> durch das Verzeichnis
/usr/proj/isabelle/polyml/sparc-solaris
zu ersetzen ist, in dem der Compiler installiert ist.
- Beispielprogramme können mit dem use Befehl eingelesen werden, also z.B.
use "blatt1.ML";
Der Compiler kann mit <CTRL>-d wieder verlassen werden.
Eine Kurzeinführung in ML ist hier zu finden.
Hinweise zu Prolog
Starten der Compiler
- In der Halle ist der Prolog-Interpreter
Eclipse installiert. Er wird mit eclipse gestartet
und mit CTRL-d beendet. Nach dem Starten sollte das
File init.pl mittels
[init].
geladen werden, das einige Flags setzt. Das Flag print_depth,
das (analog zu ML) die Größe der ausgegebenen Ausdrücke
kontrolliert, kann mittels
set_flag(print_depth, <Tiefe>).
verändert werden.
- Für das Arbeiten zu Hause empfiehlt sich das frei erhältliche
SWI-Prolog. Es
wird nach der Installation mit pl gestartet und mit
CTRL-d beendet.
- Unter SWI-Prolog kann die Größe der ausgegebenen
Ausdrücke mit
set_prolog_flag(toplevel_print_options, [max_depth(<Tiefe>)]).
verändert werden.
Einlesen von Prolog-Files
Prolog-Files (die mit dem Suffix .pl enden müssen) können mittels
[<Filename>].
geladen werden, wobei <Filename> den Filename ohne
das Suffix .pl bezeichnet, z.B.
[einfuehrung].
Weitere Hinweise sind in der Einführung
zu finden (siehe auch das dazugehörige Prolog-File).
|
