minlog 4.0.99.20100221-5.2 / usr / share / minlog / src / prologue.scm

; minlog3j.scm
; 00-01-15

(begin
(display "This is Minlog, Version 1.03j of January 2000") (newline)
(display "Copyright (C) 2000 H. Schwichtenberg") (newline)
(display "email schwicht@rz.mathematik.uni-muenchen.de") (newline)
*the-non-printing-object*)

; Inhalt:
;  1. Vorbereitungen		           list.scm
;  2. Typen		                   typ.scm
;  3. Variablen                            var.scm
;  4. Programmkonstanten                   pconst.scm
;  5. Praedikaten- und Funktionssymbole    psym.scm
;  5-1. Praedikatensymbole
;  5-2. Funktionssymbole
;  6. Terme                                term.scm
;  6-1.  Aufbau und Zerlegung
;  6-2.  Normalisierung
;  6-3.  Termersetzung
;  6-4.  Alpha-Gleichheit
;  6-5.  Darstellung
;  6-6.  Pruefung
;  6-7.  Substitution
;  6-8.  Unifikation
;  6-9.  Einseitige Unifikation
;  7. Formeln und Komprehensionsterme      formula.scm
;  7-1.  Aufbau und Zerlegung
;  7-2.  Normalisierung
;  7-3.  Alpha-Gleichheit
;  7-4.  Darstellung
;  7-5.  Einlesen
;  7-6.  Pruefung
;  7-7.  Substitution
;  8. Axiome                               axiom.scm
;  9. Globale Annahmen und Theoreme        globalass.scm
; 10. Beweise                              proof.scm
; 10-1.  Aufbau und Zerlegung
; 10-2.  Normalisierung
; 10-3.  Substitution
; 10-4.  Darstellung
; 10-5.  Pruefung
; 11. Partielle Beweise                    pproof.scm
; 12. Resolution mit Hornklauseln          hres.scm
; 13. Ein Beweiser fuer Aussagenlogik      prop.scm
; 14. Hindleys Typinferenz-Algorithmus     type-inf.scm
; 15. Beweissuche und Logikprogrammierung  quant.scm
; 16. Extrahierte Terme                    ets.scm
; 17. A-Uebersetzung                       atr.scm
; 18. Simultane freie Algebren             sfa.scm

; 00-01-16;  Simultane freie Algebren eingebaut (nach Holger Benl)
;  Dazu: closure eingefuegt.  add-variable nimmt jetzt mehrere Symbole + Typ.
;  arg-types jetzt in der Form (arg-types type <n>) mit n optional.
;  final-val-type eingefuegt.  reset wirkt auch fuer GROUND-TYPES.
;  (set-minus-wrt eq? ...) ersetzt durch (set-minq ...), etc
;  introduce-simultaneous-free-algebras (kurz isfas) eingefuegt.

; 99-12-14: In petite chez scheme verhaelt sich assq anders als in lmuscheme.
;  (assq 'test '(4 (test 6))) -> 
;  Error in assq: improperly formed alist (4 (test 6)).
;  (Vorlaeufige) Korr: statt (assq wrong-u oc) (assq wrong-u (reverse oc))

; 99-12-06:  Klammerfehler in strip korrigiert.

; 99-07-22:  In pterm-and-context-to-pg-ec-and-new-pterm-and-npgs einen
;   Fehler korrigiert (argument context eingefuegt).

; 99-07-19: In imp-intro equal? durch alpha-=-nfs? ersetzt

; 99-05-05  In var-to-index eine Abfrage eingebaut, ob eine Variable
;   vorliegt.  Andernfalls ist das Ergebnis 0.  ec-item-psym-substitute
;   korrigiert.  minpr.scm eingearbeitet.
;   t-expr-psym-substitute-generating-new-global-assumptions korrigiert.

; 99-04-16  Mehrstellige klassische Existenzquantoren eingefuehrt.  Grund:
;   Bei der Programmextraktion aus klassischen Beweisen ist exc i exc j
;   ~all i~~all~ j, also nicht Negation einer rein generalisierten Formel.

; 99-04-11:  tensor als Alternative zu & eingefuehrt.  Grund: 
;   fold-formula und unfold-formula sollen invers zueinander sein.  Ohne
;   Tensor haette man (all n.A -> B -> F) -> F folds into exc n.A & B
;   unfolds into (all n.A & B -> F) -> F.  Also: exc n.A ! B steht fuer
;   (all n.A -> B -> F) -> F, und exc n.A & B fuer (all n.A & B -> F) ->
;   F.  steht.  In Formeln wird tensor beliebig erlaubt (auch in Hinblick
;   auf spaetere Erweiterungen in Richtung lineare Lambda-Terme).  In
;   Beweisen darf tensor nur im Kontext exc n.A1 ! A2 ! .. ! An vorkommen,
;   und diese Formel wird mit (all n.A1 -> A2 -> .. -> An -> F) -> F
;   identifiziert.  Dann exc-intro2-thms: all n.A -> B -> exc n.A tensor B
;   exc-elim2-thms: (exc n.A ! B) -> (all n.A -> B -> C) -> C Ferner
;   Duplikation von Code fuer excl (logisch) und exca (arithmetisch)
;   moeglichst vermieden.  Zum Beispiel funktioniert exc-elim fuer beide.

; 99-04-10:  search bzgl. partieller Variablen korrigiert.

; 99-04-03:  Klassische Existenzquantoren exc (arithmetische Version) 
;   und excl (logische Version) eingefuehrt.  Sie werden als Abkuerzungen
;   aufgefasst, insbesondere als alpha-gleich angesehen.  unfold-formula
;   und fold-formula eingefuehrt.  Bei assume und strip wird soweit wie 
;   noetig ausgefaltet;  bei nf und display wird nicht ausgefaltet.  
;   rm-ex getilgt;  stattdessen ex-to-exc und ex-to-excl.

; 99-03-30: imp-intro korrigiert (und Argumente vertauscht) und 
;   c-intro statt intro eingefuehrt (analog c-abst).  Terminologie:
;   efq-thm, stab-thm fuer efq, stab.  efq, stab fuer efq-with-psym,
;   stab-with-psym.

; 99-03-27: Praedikatenkonstante und Praedikatenvariablen unterschieden
;   (Grund: in efq-log: bot -> p darf fuer bot nicht substituiert werden).

; 99-03-23: THEOREM-CONSTANTS, THEOREM-SCHEMA,CHEME-SYMBOLS, 
;   GLOBAL-ASSUMPTION-SCHEME-SYMBOLS eingefuehrt.  save speichert Theoreme.
;   Logisches Falsum (bot) als psym eingefuehrt (Grund u.a.: A-Uebersetzung).
;   p, p1,p2,p3 sind nullstellige Praedikatensymbole (q res. fuer 1-stellige).
;   efq-log: bot -> p, stab-log: ((p -> bot) -> bot) -> p sind GA-Schemata,
;   ebenso efq: F -> p, stab: ((p -> F) -> F) -> p.
;   cases-log: (p -> p1) -> ((p -> bot) -> p1) -> p1 ist Theorem-Schema,
;   dessen Beweis die globale Annahme stab-log (fuer p1) verwendet.
;   efq-thm: all pp^.F -> pp^, stab-thm: all pp^.((pp^ -> F) -> F) -> pp^ sind 
;   Theoreme.  efq-axiom-at und stab-axiom-at getilgt (unnoetig wegen efq-log).
;   prop verwendet bei bot efq-log und bei F efq-thm bzw. efq, 
;   ebenso bei bot stab-log und bei F stab-thm bzw. stab.
;   (search m (u1 m1) (u2 m2) ...) laesst fuer ui auch Theoreme zu, nicht aber
;   Schemata (Grund: Unifikation wuerde uferlos).  Die gewuenschte Instanz
;   soll sich der Benutzer selbst ueberlegen und als Theorem abspeichern.

; 99-03-09: def-nat, extends_nat korrigiert.  formula-check-to-string 
;   korrigiert.  t-expr-psym-substitute korrigiert.

; 99-03-12: Praedikatensymbole eingefuehrt, analog zu Funktionssymbolen.
;   Stelligkeit eines Praedikatensymbols:  tau1 -> tau2 -> prop
;   Komprehensionsterme gebraucht, zur Substitution fuer Praedikatensymbole.
;   Keine Typvariablen (Grund: Typen werden aus Variablennamen erschlossen).
;   Boolesche Variable p,q in pp,qq umbenannt (um p,q frei zu haben).
;   efq-axiom-at und stab-axiom-at hinzugefuegt (wegen der Praed.symbole)

; 99-03-01: Am Ende von add-ground-type ein n durch k ersetzt.  In use-with
;   2mal new-vars eingefuegt (war vergessen).  program-scheme-check korrigiert.

; 98-12-01: Bei use-with und inst-with: freie Variable ausserhalb des 
;   geordneten Kontexts in den Termen zugelassen.  Geordnete Kontexte
;   von neu erzeugten Zielen korrigiert (neue Variable hinzugefuegt).
;   Beweisterme duerfen jetzt auch Variablen frei enthalten (um Logik in
;   Grundtypen zu ermoeglichen, fuer die man keine Konstante hat).
;   Bei drop: unnoetig gewordene Variable werden automatisch entfernt.

; 98-11-29: (reset) eingefuehrt: setzt die globalen Variablen VARIABLES, 
;   VAR-PLISTS, PROGRAM-CONSTANTS, FUNCTION-SYMBOLS, AXIOM-CONSTANTS,
;   AXIOM-SCHEME-SYMBOLS, GLOBAL-ASSUMPTIONS wieder 
;   auf ihren urspruenglichen Wert.
;   add-global-assumption-with-et (kurz agawet) hinzugenommen.
;   Entsprechend elim-pterm-to-et-and-formula angepasst.

; 98-11-24: Um unter Implementierungen mit beliebiger
;   Standard-Gross-bzw.-Kleinschreibung (z.B. Bigloo vs LMU-Scheme)
;   lauffaehig zu sein, Symbole wie immer erst mit 'test in die
;   Standard-Gross-bzw.-Kleinschreibung transformieren und erst dann
;   mit string->symbol einen string daraus herstellen.  Deshalb z.B.
;   "undef_"  ersetzt durch  (symbol->string 'undef_).
;   Ferner (damit der get-Befehl sein Ziel aus einer AListe von Zielen 
;   findet) auch die Benennung der Ziele in die
;   Standard-Gross-bzw.-Kleinschreibung transformiert.  Deshalb z.B.
;   "KERNEL"  ersetzt durch  (string->symbol 'kernel).
;   In scan einen Test auf standard-case-of-implementation eingebaut.
;   c-# durch c-@ ersetzt (# nicht erlaubt im revised^5 report)

; 98-11-19: add-ground-type, nat-simrec-at korrigiert (fuer Termfamilien)

; 98-10-20: obj-to-long-normal-form und normal-app-expr-to-obj umbenannt
;   in reify und reflect.  Den Einbau von Termfamilien (s. Nada-Arbeit)
;   auch im Text beruecksichtigt.  obj-to-term getilgt.  In Termen statt
;   Numeralen wie 27 jetzt (num 27), das zu einer Termfamilie auswertet.

; 98-05-28:  Fehler in prop-i korrigiert (pterm-of-efq-at statt
;   neuer globaler Annahme verwendet).  unstrip korrigiert.

; 97-08-26: search korrigiert: Beim Aufruf sind sig-vars nicht leer.
;   Ferner: Bei Annahmen aus dem geordneten Kontext darf die Vielfachheit
;   auch 0 sein, damit man ausblenden kann.

; 97-04-29: and-strict durch and_strict ersetzt (Tippfehler)

; 97-03-03: search.scm durch searchex.scm ersetzt, das jetzt auch 
;   (konstruktive) Existenzquantoren behandeln kann.  In soln-and-pterm-b
;   (or forb-vars ...) ersetzt durch (or (pair? forb-vars) ...).

; 97-02-20: simp korrigiert: bei Gleichungen wird nur die rechte durch
;   die linke Seite vereinfacht. simptrue, simpfalse getilgt (ueberfluessig)
;   inst-with eingefuegt und deshalb inst getilgt

; 97-02-19: Definition supertotal geaendert: Werte streng total.
;   Grund: supertotale Werte sind konstant, also nicht sinnvoll.
;   search.scm eingefuegt (in quant.scm)

; 97-02-06: term-to-critical-subterm-as-list-with-type korrigiert:
;   Abfrage pair? eingefuegt.  Ferner: Da memq assoc etc im negativen Fall
;   #f ergeben, an diesen Stellen (pair? info) wieder durch info ersetzt.

; 97-02-03: pattern-unify-by-occurs-check-and-pruning korrigiert:
;   Abfrage pair? eingefuegt (auch noch an zwei anderen Stellen, bei memq)

; 97-01-31: hres.scm (Resolution mit Hornklauseln) herausgenommen.

; 97-01-29: tdeg.scm eingearbeitet. Das heisst
;   Einen neuen Totalitaetsgrad eingefuehrt: streng total.
;   Grund: Konstruktor con bei listen erfuellt  def(con bot(con 7 eps)).
;   Also:  (con a^) ist fuer beliebiges  a^  total (nicht supertotal).

; 97-01-28: Abkuerzungen fuer lange Zielsymbole eingefuehrt.
;   simp.scm eingearbeitet: simptrue, simpfalse, simp. Dafuer:
;   '=-at 'eq-at als axiom-scheme-symbols hinzugefuegt.
;   Entsprechend axiom-scheme-check angepasst.  Hinzugenommen:
;   =-Axiomenschema (beweist  all xs,x,y.x=y -> A(y) -> A(x)) und
;   eq-Axiomenschema (beweist  all xs,x,y.eq_nat x y -> A(y) -> A(x))
;   Ferner: c-eq (analog c-=).
;   In globalass.scm hineingenommen: atomtrue (beweist all pp^.pp^ -> pp^=true)
;   sowie atomfalse (beweist  all pp.(pp -> F) -> pp=false).
;   Bei if-symbol? eingefuegt: =-symbol? und eq-symbol?
;   In ets.scm angepasst: axiom-scheme-form-to-et, =-at-to-et
;   Weitere Korrekturen in ets.scm: Abfrage (eq? 'nulltype type) eingefuegt.

; 97-01-11: if-type-output-string "[...]" verwendet,
;   um auf die besondere Ausgabe [...] bei if-type hinzuweisen.

; 97-01-08: Reihenfolge der Abstraktionen bei parse-term korrigiert.
; - In c-abst den Test auf Partialitaet der Variablen entfernt. Grund:
;   Eine Unterscheidung totale/nicht totale Variable ist hier nicht
;   noetig, da der Wert eines Lambda-Objektterms als Argumente immer alle
;   stetigen Funktionen hat. 
; - In (et proof) werden jetzt neue Objektvariable nur fuer 
;   Annahmenvariablen mit rechnerischem Gehalt gebildet.
; - In pterm-to-et c-abst-without-check verwendet.
; - In elim-pterm-display-to-formula-and-rule und ebenso in
;   elim-pterm-to-et-and-formula die Abfrage assumption-variable?
;   durch Frage nach Vorkommen der Variable im Kontext ersetzt;  das
;   erspart manchmal die Normalisierung.  Abfrage auf nulltype eingebaut.

; 97-01-04: Felix Joachimskis add.scm eingearbeitet:
; Eingefuegt: display-more, 
;   ground-type?, program-scheme-symbol?, axiom-scheme-symbol?, is-used?,
;   add-axiom-constant, aac, remove-axiom-constant, rac, 
;   add-axiom-scheme-symbol, remove-axiom-scheme-symbol,
; Mit is-used? neu formuliert: add-ground-type, add-variable,
;   add-program-constant, add-self-evaluating-program-constant,
;   add-function-symbol, add-global-assumption
; Eingefuegt: undo ohne Argument, macht den letzten Schritt rueckgaengig.
; Eingefuegt: display-current-goal, dcg, split-iterated, close-proof
; cases bei Aufruf ohne test korrigiert (neu: first-if-term-in).

; 96-09-17: Verwendung von letrec in nat-ind-at und nat^-ind-at korrigiert.

; 96-08-23: In if-nat etc. (auch in agt) folgende Regeln hinzugefuegt:
;   [if test then y else y] -> y  (falls test syntaktisch total ist)
;   [if [if test then con else alt] then y else z] -> 
;     [if test then [if con then y else z] else [if alt then y else z]]
;   Ferner speziell bei if-boole:
;   [if test then true else false] -> test

; 96-08-20: In agt eq-type in eq_type umbenannt (wegen minus und
;   Konsistenz mit eq_nat). Ferner if-type-output-string "xx" verwendet,
;   um auf die besondere Ausgabe [...] bei if-type hinzuweisen.

; 96-08-19: Definition split korrigiert (else war falsch).

; 95-10-09: assoc-wrt und member-wrt korrigiert: Wert #f statt '().

; 95-09-26: Darstellung von Paar- und Komponententermen verbessert.
;   @ durch # und c-pair durch c-# ersetzt. parse-object, parse-more,
;   term-to-string und op-and-args-and-string-and-strings-to-string angepasst.

; 95-09-25: type-to-new-partial-variable korrigiert. Es erzeugt jetzt
;   einen string, der als Variablenname in Frage kommt (also ohne Klammern
;   und ohne "-"). Deshalb neu hinzugefuegt: type-to-string-for-name.

;   type-to-efq-variable eingefuehrt, mit angehaengtem 000. Grund: Bei et
;   fuer ein efq-axiom  F -> ex n.n=0 braucht man die IH fuer eine Instanz.
;   Hierfuer wird jetzt die spezielle Variable n000 genommen.

; 95-09-24: minus-nat, max_nat und min_nat eingefuegt. Polynomnormalform
;   verbessert. term-to-undef-sources liefert eine Liste aller Teilterme
;   eines Terms, die zu undef_nat fuehren koennten.

; 95-09-16: 'undef 'false 'true ersetzt durch undef false true.
;   undef-boole, undef-nat ersetzt durch undef_boole, undef_nat. Grund:
;   In der Ausgabe verwendete Symbole duerfen kein "-" enthalten (wegen minus).
;   Bei if-nat kann "-" bleiben, da in der Ausgabe [...] verwendet wird.
;   eq-nat, leq-nat, less-nat ersetzt durch eq_nat, leq_nat, less_nat.
;   imp-fsym und and-fsym ersetzt durch imp_fsym und and_fsym und als
;   nicht strikte Funktionen operierend gemacht. and-nonstrict getilgt.
;   Ausgabe "[=" bei extends_nat und extends_boole getilgt.

; 95-09-15: Korrigiert: pred-nat hat Totalitaetsgrad 0.

; 95-09-08: In prop.scm Existenzquantoren zugelassen. Fehler im Quantorenfall
;   korrigiert. efq-at eingefuegt. (efq-at formula) erzeugt einen Beweis
;   von F -> A. Dabei wird fuer atomare Formeln die globale Annahme
;   efq: all pp^.F -> pp^ verwendet. formula darf Existenzquantoren enthalten.

; 95-09-06: all-all^-axiom korrigiert: die freien Variablen in der
;   all^-Formel werden vorn abgebunden. Neu: (cases-all^). Erwartet eine 
;   (nicht notwendig geschlossene) Zielformel all x^ A(x^) mit x^ von einem
;   Grundtyp. Erzeugt werden zwei neue Ziele:  A(undef)  und  all x A(x).
;   Bei (cases test) Pruefung eingefuehrt, ob der Term test vom Typ boole
;   ist und nur freie Variablen aus dem geordneten Kontext enthaelt.
;   Bei  inst  wird die instanziierte Hypothese  u  jetzt mit  ui  bezeichnet.

; 95-09-04: def-nat und extends-nat hinzugenommen (waren vergessen). 

; 95-08-29: if-nat hinzugenommen (war vergessen). 
;   Vor c-ex befand sich ein (ueberfluessiges) <-Zeichen: getilgt.
;   +-nat durch plus-nat ersetzt (fuehrt in UMB-Scheme zu Problemen)
;   Da (z.B. in UMB-Scheme) #f und () verschieden sind, an vielen Stellen z.B.
;   info durch (pair? info) ersetzt. Ferner z.B. in globalass.scm 
;   (formula-to-free y) durch (pair? (formula-to-free y)) ersetzt.

; 95-07-14: term-to-monoms korrigiert: falls nicht zusammengesetzt,
;   wird (list (list term)) zurueckgegeben. suc-nat? wieder hinzugenommen
;   (war vergessen). <-strict-nat korrigiert

; 95-07-14: Termersetzungsregeln fuer nat korregiert und verbessert. 
;   Grund: Bisher reduzierte n^+m <= n^+k auf m <= n; fuer n^=undef
;   muesste aber undef-boole herauskommen. Ferner war falsch: polyn-to-const
;   Ferner: if-boole eingefuegt (war vergessen)

; 95-06-30: nat-simrec-at korrigiert (n-1 statt n im step)

; 95-03-30: et.scm (Extrahierter Term nach Benl und Niggl) eingefuegt.
;   Entsprechend cons-arrow-et (mit c-arrow-et) und cons-star-et so 
;   definiert, dass Nulltypen verschluckt werden.

; 95-03-15: cut eingefuegt.

; 95-02-24: In quant.scm bei der Unifikation fuer Muster Reihenfolge der
;   zu abstrahierenden Variablen korrigiert.

; 95-01-20: agt1 mit quasiquote formuliert. Dabei wird mit (agt 'obj) jetzt
;   auch if-obj fuer den neuen Grundtyp obj definiert.

; 95-01-18: In parse-object im sonst-Fall eine Abfrage function-symbol?
;   eingefuegt. use-with geaendert: es wird auch abgeprueft, ob 
;   ein benutzter Term nur freie Variable im geordneten Kontext enthaelt.

; 94-04-28: Im Parser Test auf unbalancierte Klammern eingefuehrt.

; 94-04-25: ets (extrahierte Terme) aufgenommen.
;   undef-at neu in PROGRAM-SCHEME-SYMBOLS; if-at veraendert

; 94-04-18: LOCAL-ASSUMPTIONS als neue globale Variable eingefuehrt:
;   Aliste der (von normalize-proof) mit gensym neu erzeugten oder
;   im Kontext vorhandenen Annahmevariablen mit ihren Typen.
;   Grund: Bei ex-elim-at muss man die Typen der in einem Beweisterm
;   freien Annahmevariablen kennen, um ihn auswerten zu koennen.

; 94-04-13: Vorbereitungen zur Einfuehrung von ets (extrahierte Terme):
;   - formula-to-types und c-list-type eingefuehrt.
;     type-to-string verbessert (nach Robert Staerk). * rechtsassoziativ.
;   - nulltype neuer Grundtyp;  leere Liste einziges Objekt.
;     obj-to-long-normal-form und normal-app-expr-to-obj geaendert.
;   - nat-rec-at, nat-simrec-at, if-at sind PROGRAM-SCHEME-SYMBOLS
;   - pair, left-comp, right-comp ersetzt durch cons, car, cdr
;   c-app, c-abst statt app, abst. c-abst analog zu c-all
;   curry, uncurry erhalten als erstes das Prozedurargument (wie list-ref)

; 94-04-08: Zerlegungsoperationen fuer (normale) Beweise eingefuehrt.

; 94-04-06: (stab-at formula) erzeugt einen Beweis von ((A -> F) -> F) -> A.
;   Dabei wird fuer atomare Formeln die globale Annahme
;   stab: all pp^.((pp^ -> F) -> F) -> pp^ verwendet.
;   (stab-arith-at formula) ersetzt in dem Beweisterm von (stab-at formula)
;   die globale Annahmenvariable stab durch stab-pterm
;   (gebildet mit boole^-ind-at).

; 94-04-02: Konstruktiver Existenzquantor ex eingefuegt. Gruende:
;   - Beweise werden direkter und sind deshalb besser zu verstehen.
;   - Automatische Uebersetzung in klassische Beweise ist moeglich: rm-ex
;   Zusaetzlicher Grundtyp existential eingefuehrt, fuer ex-Formeln.

; 94-03-09: pattern-unify korrigiert.
;   remove-variable und remove-ground-type hinzugefuegt.
;   normalize-formula veraendert: (atom undef-boole) wird zu (atom false)
;   normalisiert (also: beide werden identifiziert). Entsprechend werden die
;   Axiome undef-to-false-axiom und false-to-undef-axiom getilgt.
;   cases verbessert;  Aufruf jetzt (cases test)

; 94-03-07: app fuer Produkttypen korrigiert. delta in def umbenannt.
;   parse-term und parse-formula (:= parse) verbessert: (pt "n<m") liefert
;   jetzt einen Term, und def ist einbezogen.
;   Alpha-= ohne gensym implementiert (nach Robert Staerk).
;   In gensym und new-variable beginnt jetzt der Index zur Unterscheidung
;   von benutzerdefinierten Variablen mit einer fuehrenden 0.
;   Bei type-to-new-partial-variable nimmt man zwei fuehrende Nullen.

; 94-03-04: c-=, c-<, c-<= so umdefiniert, dass sie die strikten
;   Relationen liefern. Grund: undef wird als endlicher Fehler gesehen
;   und sollte deshalb durchgereicht werden.
;   Ferner:  pp in pproof umbenannt (pp gibt es schon im MIT-Scheme)
;   error umbenannt in myerror ('error' ist nicht standard)

; 94-03-02: c-undef und undef? (fuer Grundtypen) hinzugefuegt.
;   all-all^-axiom (fuer Grundtypen) und cases verbessert.
;   Ueberall undefined in undef umbenannt.

; 94-02-28: truth-axiom in die Beweissuche eingebaut.

; 94-02-22: Beweispruefung angepasst an: Axiomenschemata duerfen
;   freie Variable enthalten. Neu: axiom-scheme-check.
;   check-and-display-proof korrigiert: Kontext wird erst nach
;   Pruefung bearbeitet. 

; 94-02-01: asepc (add-self-evaluating-program-constant) hinzugenommen
;   Die Angabe des Totalitaetsgrades und der Darstellungszeichenreihe
;   ist nicht mehr notwendig;  Standardwerte: 0 bzw. das in eine
;   Zeichenreihe umgewandelte Symbol.

; 93-10-11: Induktion fuer nat und boole verbessert (nach Berger und Niggl)
;   Es wird nicht mehr der gesamte geordnete Kontext abgebunden, sondern
;   nur noch die freien Variablen. Ferner wird eine modifizierte boolesche
;   Induktion (mod-boole-ind-at (all pp A(pp))) als Axiom eingefuehrt: 
;   all pp.(pp -> A(true)) -> (~pp -> A(false)) -> A(pp) statt
;   A(true) -> A(false) -> all pp A(pp) 
;   Dadurch werden Fallunterscheidungen in Beweisen kuerzer. Deshalb entfernt:
;   cases-boole, cases-boole^, cases-term, cases, cases-new. Neu: cases

; 93-10-11: Entfernt: immed. Grund: prop ist allgemeiner

; 93-05-24: c-if und c-def fuer beliebige Grundtypen verwendbar gemacht.
;   Parser angepasst: (c-if pred then-part else-part) statt
;   (app 'if-nat pred then-part else-part)

; 93-04-13: Abschnitt 10. `Beweise' verbessert und korrigiert (dp, cdp).
;   Hauptpunkt: Die Benennung gebundener Variablen in Beweistermen soll
;   keine Rolle spielen, wohl aber in Formeln: dort werden der Typ und
;   der Totalitaetsgrad durch den Variablennamen bestimmt.

; 93-01-13: inst zur Instanziierung von Allhypothesen und split-hyp zur
;   Aufspaltung von konjunktiven Hypothesen hinzugefuegt.

; 92-12-30: undefinierte boolesche Terme in Formeln zugelassen. 
;   Grund: undefiniert spielt die Rolle eines Fehlerobjekts, nicht einer
;   nichtterminierenden Rechnung.
;   Entsprechend Axiome undef-to-false-axiom und false-to-undef-axiom
;   hinzugenommen.

; 92-12-20: Hudelmaiers Beweissuchverfahren fuer die minimale Aussagenlogik
;   implementiert, in prop.scm
; - Typinferenz (nach Hindley) implementiert, in type-inf.scm

; - Zur Effizienzsteigerung  wird nach der ersten Pruefung z.B. u17
;   in eine Liste CHECKED-ASSUMPTION-VARIABLES eingetragen
; - gensym erhaelt einen globalen Zaehler gensym-count, der bei jedem
;   Aufruf von set-goal wieder auf 9 gesetzt wird. Der Benutzer sollte dann
;   nur Variablennummern <10 verwenden, um Kollisionen zu vermeiden.
;   Grund: Man kann dann (strip) in Taktik-Dateien verwenden.
; - (new-hypsym) durch (gensym "u") ersetzt.

; 92-11-25 und 92-12-04: Angepasst an das neue MIT--SCHEME.
; - in 6-6 bei scan-term char-upcase getilgt (da beim neuen SCHEME die
;   Symbole klein geschrieben werden). Ebenso in 7-5.
;   Beispiel: 'Test => test, aber (string->symbol "Test") => Test.
; - Ueberall string-downcase getilgt.
; - "U", "X", "C-" durch kleingeschriebene strings ersetzt.
; - op-and-args-and-string-and-strings-to-string korrigiert (vorher war auf
;   left-assoc? nicht bezug genommen).
; - in new-hypsym (frueher: newhypsym) "HYP" durch "u" ersetzt.

; Geaendert gegenueber nat4.scm
; - Produkttypen sind hinzugenommen. Grund: Durch simultane Rekursion werden
;   Objekte von Produkttypen definiert. Diese Auffassung ist notwendig,
;   um solche Programme effektiv ausfuehren zu koennen.
; - Entsprechend wird die Konjunktion von Formeln hinzugenommen. Grund: Beweise
;   durch simultane Induktion sollen als effektive Programme ausgefuehrt
;   werden koennen.
; - eq-nat testet seine Argumente modulo Assoziativitaet und Kommutativitaet
;   von + und *. Ferner wird die Distributivitaet von * ueber +
;   ausgenutzt.
; - Abschnitt 13: Resolution ist vorlaeufig hinausgenommen, in resolution.scm

; Geaendert gegenueber nat3.scm
; - Ein Parser fuer Terme und Formeln ist hinzugenommen.
; - immed ist wieder hinzugenommen, erweitert fuer den Fall, dass die
;     Zielformel mit truth endet.
; - Hinzugefuegt: (cases atom). Ersetzt das Ziel durch zwei neue:
;     atom -> goal-formula[boolean-kernel/true]
;     (atom -> F) -> goal-formula[boolean-kernel/false]
; - Hinzugefuegt: (cases-boole boolean-term). Ersetzt das Ziel durch zwei neue:
;     boolean-term=true -> goal-formula[boolean-term/true]
;     boolean-term=false -> goal-formula[boolean-term/false]
; - (expr-substitute expr subst) verarbeitet jetzt eine Aliste
;     subst = ((expr11 expr12) (expr21 expr22) ...): Substituiert werden
;     simultan die linken Seiten der Aliste subst an allen
;     Stellen, an denen in ihnen keine freie Variable abgebunden ist, durch
;     die entsprechenden rechten Seiten. Umbenannt wird genau dort,
;     wo die Substitution eine vorher freie Variable in den Bindungsbereich
;     eines Quantors befoerdern wuerde.
; - Formelschreibweise: Z.B.  all n,m n=m  und  all n.n=0 -> 0=n
;     Punkt bedeutet: Wirkungsbereich des Allquantors bis zum Ende der
;     folgenden (klammerfrei geschriebenen) Implikation.

; Geaendert gegenueber nat2.scm
; - Resolution mit Hornklauseln fuer das  -> all -Fragment ist hinzugefuegt.
;     Die Zielformel muss hier atomar sein, also ggf erst (strip) anwenden.
; - Ebenfalls ist die klassische Resolution hinzugefuegt.
;     Der geordnete Kontext muss hier leer sein, also ggf erst (unstrip)
;     anwenden. Ein Beweistermen wird nicht aufgebaut: Stattdessen wird
;     im Erfolgsfall eine neue globale Annahme Resolution-proof-for-<formula>
;     verwendet.
; - Beim interaktiven Beweisen wird immer das oberste Ziel auf dem Stapel
;     angesprochen: Mit  (get <goal-name>)  kann man ein beliebiges Ziel
;     nach oben bringen.
; - strip, unstrip und drop sind hinzugefuegt
; - Beweise werden jetzt durch 3er-Vektoren statt durch Listen dargestellt.
; - Simultane Substitution fuer Terme, Formeln und Ausdruecke hinzugefuegt:
;     (term-substitute term subst), (formula-substitute formula subst) und
;     (expr-substitute term subst)
;     Ebenfalls wird die simultane Ersetzung in Ausdruecken hinzugefuegt:
;     (t-expr-replace expr subst)

; Geaendert gegenueber nat.scm
; - eta-Konversionen eingefuehrt
; - (atom r) nur mit syntaktisch totalem r zulassen. Deshalb: <-nat wie =-nat
;     als supertotales Funktionssymbol verwenden, damit <-Atomformeln gebildet
;     werden koennen. Zusaetzlich: <-strict-nat
; - In interaktiven Beweisen in den Zielen nicht-normale Terme zulassen
;     (wegen besserer Lesbarkeit, Z.B x+4 statt (S(S(S(Sx)))) ). Zusaetzlich:
;     normalize-goal (kurz ng), das alle Terme im Ziel normalisiert
; - Bei Korrektheitspruefungen in Beweisen immer pruefen, ob die
;     Normalformen gleich sind.
; - c-all wird andersherum geschrieben: (c-all symbol1 symbol2 ... formula)
; - * durch ^ ersetzen, um Verwechslungen mit mal zu vermeiden.
; - term-to-bound, formula-to-bound und expr-to-bound sind weggelassen,
;     da sie nicht mehr gebraucht werden.
; - Zur besseren Lesbarkeit (und zur Vereinfachung der Definition von
;     term-to-t-deg) soll die mit lambda abstrahierte Variable immer total
;     sein. Eine Unterscheidung totale/nicht totale Variable ist hier nicht
;     noetig, da der Wert eines Lambda-Objektterms als Argumente immer alle
;     stetigen Funktionen hat. (Spaeter bei Beweistermen sagt die Formel, ob
;     totale oder partielle Objekte gemeint sind.)

; Ziele:
; - Interaktive Beweisentwicklung => Beweis vom Rechner geprueft,
;     Beweis als Objekt vorhanden, also manipulierbar
; - Normalisierung von Beweisen effizient implementieren =>
;     Experimente moeglich
; - Moeglichst viel Beweisarbeit auf die rechnerische Ebene schieben
;     und Termersetzung verwenden.
;     Schnittstelle allgemeines Logiksystem -- spezielle Anwendung definieren.
;     Kriterien fuer Termersetzung:
;     * Terminierend
;     * geschlossener Term der Stufe 0 -> (eindeutige) Ziffer
;     * Bedeutungserhaltend (bei bekannter Bedeutung in unserer festen
;         Semantik)
;     * Nuetzlich fuer Beweise

; Technische Punkte:
; - Wegen leichterer Lesbarkeit der Formeln:
;     * Benennung quantifizierter Variablen nicht aendern
;     * Typ einer Objektvariablen aus dem Symbol ablesen.
; - Es ist erlaubt, dass auf einem Zweig (in Term, Formel, Herleitung)
;     dieselbe gebundene Variable mehrmals auftritt.