<?xml version="1.0" encoding="ISO-8859-1"?>
<!-- This DTD was generated by class org.qedeq.parser.SyntaxParser        -->
<!-- at 2003-05-04T23:54:21+0200.                                          -->

<!-- Project Principia Mathematica II - *pmii* - http://www.qedeq.org      -->
<!-- Copyright 2001, 2002 Michael Meyling (michael@meyling.com)            -->

<!-- This file is part of *pmii*.                                          -->

<!-- Permission is granted to copy, distribute and/or modify this document -->
<!-- under the terms of the GNU Free Documentation License, Version 1.2    -->
<!-- or any later version published by the Free Software Foundation;       -->
<!-- with no Invariant Sections, no Front-Cover Texts, and no              -->
<!-- Back-Cover Texts. -->

<!-- eine Formel der Prädikatenlogik -->
<!ENTITY % FORMULA "(
	(
		PROP |
		NOT |
		AND |
		OR |
		IMPL |
		EQUI |
		PREDVAR |
		FORALL |
		EXISTS |
		PATTERN
	)
)" >

<!-- Startterminal -->
<!ELEMENT MODULE (
	HEADER,
	IMPORTS?,
	USEDBY?,
	PARAGRAPHS
)>

<!-- Kopfsatz eines Moduls -->
<!ELEMENT HEADER (
	SPEC,
	HEADLINE,
	DESCRIPTION,
	EMAIL,
	AUTHORS
)>

<!-- Spezifikation eines Moduls -->
<!ELEMENT SPEC (
	NAME,
	VERSION,
	VERSION,
	LOCATIONS
)>

<!-- Name -->
<!ELEMENT NAME (
	#PCDATA
)>

<!-- Textatom, ein beliebiger Text -->
<!ELEMENT text ( #PCDATA )>

<!-- Versionsnummer im Format nn.nn.nn -->
<!ELEMENT VERSION (
	#PCDATA
)>

<!-- Liste von Modul-URLs -->
<!ELEMENT LOCATIONS (
	LOCATION+
)>

<!-- relative oder absolute URL, die auf ein Modul zeigt -->
<!ELEMENT LOCATION (
	#PCDATA
)>

<!-- Titel des Moduls -->
<!ELEMENT HEADLINE (
	#PCDATA
)>

<!-- Beschreibung des Moduls ("abstract") -->
<!ELEMENT DESCRIPTION (
	#PCDATA
)>

<!-- Email-Adresse -->
<!ELEMENT EMAIL (
	#PCDATA
)>

<!-- Liste von Autoren -->
<!ELEMENT AUTHORS (
	AUTHOR+
)>

<!--  -->
<!ELEMENT AUTHOR (
	text,
	EMAIL
)>

<!-- Liste der importierten Module -->
<!ELEMENT IMPORTS (
	IMPORT+
)>

<!-- Angaben zu einem zu importierenden Modul -->
<!ELEMENT IMPORT (
	SPEC,
	LABEL
)>

<!-- Anker, auf den verwiesen werden kann -->
<!ELEMENT LABEL (
	#PCDATA
)>

<!-- Liste der importierten Module -->
<!ELEMENT USEDBY (
	SPEC+
)>

<!-- Abschnitte -->
<!ELEMENT PARAGRAPHS (
	PARAGRAPH*
)>

<!-- Abschnitt -->
<!ELEMENT PARAGRAPH (
	text?,
	(
		ABBREVIATION |
		AXIOM |
		DECLARERULE |
		PROPOSITION
	),
	text?
)>

<!-- Definition einer Abkürzung -->
<!ELEMENT ABBREVIATION (
	%FORMULA;,
	%FORMULA;
)>

<!ELEMENT FORMULA (
	%FORMULA;
)>

<!-- Aussagenvariable -->
<!ELEMENT PROP (
	#PCDATA
)>

<!-- numerisches Atom, eine ganze Zahl -->
<!ELEMENT number ( #PCDATA )>

<!-- Negation -->
<!ELEMENT NOT (
	%FORMULA;
)>

<!-- Konjunktion -->
<!ELEMENT AND (
	%FORMULA;,
	%FORMULA;
)>

<!-- Disjunktion -->
<!ELEMENT OR (
	%FORMULA;,
	%FORMULA;
)>

<!-- Implikation -->
<!ELEMENT IMPL (
	%FORMULA;,
	%FORMULA;
)>

<!-- Äquivalenz -->
<!ELEMENT EQUI (
	%FORMULA;,
	%FORMULA;
)>

<!-- Prädikatsvariable -->
<!ELEMENT PREDVAR (
	number,
	L
)>

<!-- Liste der Subjektvariablen -->
<!ELEMENT L (
	VAR*
)>

<!-- Subjektvariable -->
<!ELEMENT VAR (
	#PCDATA
)>

<!-- Allquantor -->
<!ELEMENT FORALL (
	VAR,
	%FORMULA;
)>

<!-- Existenzquantor -->
<!ELEMENT EXISTS (
	VAR,
	%FORMULA;
)>

<!-- Pattern-Variable -->
<!ELEMENT PATTERN (
	#PCDATA
)>

<!-- Festlegung eines Axioms -->
<!ELEMENT AXIOM (
	%FORMULA;
)>

<!-- Deklaration einer neuen Regel -->
<!ELEMENT DECLARERULE (
	text,
	text,
	LINK*
)>

<!-- Referenziert ein Axiom, Satz, etc. -->
<!ELEMENT LINK (
	#PCDATA
)>

<!-- mathematischer Satz mit Beweis -->
<!ELEMENT PROPOSITION (
	SENTENCE,
	PROOF
)>

<!-- mathematischer Satz -->
<!ELEMENT SENTENCE (
	%FORMULA;
)>

<!-- Beweis eines mathematischen Satzes -->
<!ELEMENT PROOF (
	LINE+
)>

<!-- Beweiszeile -->
<!ELEMENT LINE (
	%FORMULA;,
	(
		ADDAXIOM |
		ADDSENTENCE |
		MODUSPONENS |
		REPLACEPROP |
		USEABBREVIATION |
		REVERSEABBREVIATION |
		RENAMEFREEVARIABLE |
		RENAMEBOUNDVARIABLE |
		REPLACEPREDICATE |
		GENERALIZATION |
		PARTICULARIZATION
	)
)>

<!-- Hinzufügen eines Axioms -->
<!ELEMENT ADDAXIOM (
	LINK
)>

<!-- Hinzufügen eines bereits bewiesenen Satzes -->
<!ELEMENT ADDSENTENCE (
	LINK
)>

<!-- Modus Ponens -->
<!ELEMENT MODUSPONENS (
	number,
	number
)>

<!-- Einsetzung für eine Aussagenvariable -->
<!ELEMENT REPLACEPROP (
	number,
	PROP,
	PROP
)>

<!-- Rückgängig machen einer Abkürzung -->
<!ELEMENT USEABBREVIATION (
	number,
	LINK,
	number
)>

<!-- Verwendung einer Abkürzung -->
<!ELEMENT REVERSEABBREVIATION (
	number,
	LINK,
	number
)>

<!-- Umbenennung einer freien Subjekvariablen -->
<!ELEMENT RENAMEFREEVARIABLE (
	number,
	VAR,
	VAR
)>

<!-- Umbenennung einer gebundenen Subjektvariablen -->
<!ELEMENT RENAMEBOUNDVARIABLE (
	number,
	VAR,
	VAR,
	number
)>

<!-- Ersetzung eines Prädikats durch eine Formel -->
<!ELEMENT REPLACEPREDICATE (
	number,
	PREDVAR,
	%FORMULA;
)>

<!-- Generalisierung -->
<!ELEMENT GENERALIZATION (
	number,
	VAR
)>

<!-- Partikularisierung -->
<!ELEMENT PARTICULARIZATION (
	number,
	VAR
)>