Element Summary
ADDAdd already proven formula. 
ANDLogical language: Logical conjunction. 
AXIOMMathematical axiom. 
AXIOM.DESCRIPTIONAdditional description. 
CLASSLogical language: Class described by property. 
CPA proofline that includes a conditional proof. 
CP.CONCLUSIONWe derive this formula as a conclusion. 
CP.HYPOTHESISWe assume this formula. 
DEFINITION_FUNCTIONDefinition of a function constant. 
DEFINITION_FUNCTION_INITIALDefinition of an basic function constant. 
DEFINITION_PREDICATEDefinition of a predicate constant. 
DEFINITION_PREDICATE_INITIALDefinition of an initial predicate constant. 
EQUILogical language: Logical equivalence. 
EXISTENTIALRule of existential generalization. 
EXISTSLogical language: Logical existential quantifier. 
EXISTSULogical language: Logical uniqueness quantifier. 
FORALLLogical language: Logical universal quantifier. 
FORMAL_PROOFA formal proof. 
FORMULALogical language: Formula. 
FORMULATYPEType for a formula. 
FUNCONLogical language: Function constant. 
FUNVARLogical language: Function variable. 
IMPLLogical language: Logical implication. 
LA proofline that derives from previous derived formulas. 
LATEXFor each supported language entry one can find a LaTeX text here. 
LINESList of proof lines. 
LINETYPEType for a proof line of a formal proof. 
MPThe rule Modus Ponens (or for short MP) is the sole rule of inference in propositional calculus. 
NODEThis part is the smallest unit and corresponds to the LaTeX item subsection. 
NODE.NAMEShort text to describe this item. 
NODETYPEType for a node. 
NOTLogical language: Logical negation. 
ORLogical language: Logical disjunction. 
PRECEDINGText that precedes the mathematical meat. 
PREDCONLogical language: Predicate constant. 
PREDVARLogical language: Predicate variable. 
PROOFAn informal proof. 
QEDEQRoot element. 
QEDEQ.BIBLIOGRAPHYLiterature references. 
QEDEQ.BIBLIOGRAPHY.ITEMSingle literature reference. 
QEDEQ.CHAPTERThis part corresponds to the LaTeX item chapter. 
QEDEQ.CHAPTER.INTRODUCTIONChapter contents description. 
QEDEQ.CHAPTER.SECTIONSection of chapter. 
QEDEQ.CHAPTER.SECTION.INTRODUCTIONSection contents description. 
QEDEQ.HEADERFile specification, information about the authors, imports of other QEDEQ modules and so on are part of the header. 
QEDEQ.HEADER.ABSTRACTModule contents description. 
QEDEQ.HEADER.AUTHORSList of authors of this module. 
QEDEQ.HEADER.AUTHORS.AUTHORName and email address of author. 
QEDEQ.HEADER.IMPORTSReferences to other QEDEQ modules that are a precondition for this one. 
QEDEQ.HEADER.IMPORTS.IMPORTA single reference to a QEDEQ module that must be imported. 
QEDEQ.HEADER.USEDBYList of QEDEQ modules which use (import) this module. 
QUANTIFIER_INTERSECTIONLogical language: Intersection about all classes that fullfil a property. 
QUANTIFIER_UNIONLogical language: Union about all classes that fullfil a property. 
REASONTYPEType for a rule that can derive a new formula. 
RENAMERename of bound subject variable at given occurrence by another one. 
RULEA new meta rule. 
RULE.CHANGED_RULEModifications to other existing rules. 
RULE.DESCRIPTIONAdditional description. 
RULE.LINKReferences to theorems or axioms. 
RULE.PROOFInformal proof for this rule. 
SPECIFICATIONFile specification of this module. 
SPECIFICATION.LOCATIONSList of locations to find the QEDEQ module. 
SUBSECTIONThis a normal LaTeX subsection of a section. 
SUBSECTION.TEXTThe LaTeX text of this subsection. 
SUBSECTIONTYPEType for a subsection. 
SUBST_FREESubstitute of free subject variable by term. 
SUBST_FUNVARSubstitute of function variable by term. 
SUBST_PREDVARSubstitute of predicate variable by formula. 
SUCCEEDINGText that succeeds mathematical meat. 
TERMLogical language: Term. 
TERMTYPEType for a term. 
THEOREMA theorem and it's proof. 
THEOREM.DESCRIPTIONAdditional description. 
TITLETitle of a text segment. 
UNIVERSALRule of universal generalization. 
VARLogical language: Subject variable. 


Simple Type Summary
EMAILTYPEType for an email. 
LEVELTYPEType for a level. 
LOCATIONTYPEType for a location. 

Schema Description


By default, local element declarations belong to this schema's target namespace.

By default, local attribute declarations have no namespace.

QEDEQ 1.01 Schema
This file is part of the project "Hilbert II" -

Copyright 2000-2013,  Michael Meyling <>.

Submit a bug or a feature.
Created by xsddoc, a sub project of xframe, hosted at