| |||||||
| DETAILS: DOCUMENTATION | | FRAMES | NO FRAMES | ||||||
| Element Summary | |
| ADD | Add already proven formula. |
| AND | Logical language: Logical conjunction. |
| AXIOM | Mathematical axiom. |
| AXIOM.DESCRIPTION | Additional description. |
| CLASS | Logical language: Class described by property. |
| CP | A proofline that includes a conditional proof. |
| CP.CONCLUSION | We derive this formula as a conclusion. |
| CP.HYPOTHESIS | We assume this formula. |
| DEFINITION_FUNCTION | Definition of a function constant. |
| DEFINITION_FUNCTION_INITIAL | Definition of an basic function constant. |
| DEFINITION_FUNCTION_INITIAL.DESCRIPTION | Additional description. |
| DEFINITION_FUNCTION.DESCRIPTION | Additional description. |
| DEFINITION_PREDICATE | Definition of a predicate constant. |
| DEFINITION_PREDICATE_INITIAL | Definition of an initial predicate constant. |
| DEFINITION_PREDICATE_INITIAL.DESCRIPTION | Additional description. |
| DEFINITION_PREDICATE.DESCRIPTION | Additional description. |
| EQUI | Logical language: Logical equivalence. |
| EXISTENTIAL | Rule of existential generalization. |
| EXISTS | Logical language: Logical existential quantifier. |
| EXISTSU | Logical language: Logical uniqueness quantifier. |
| FORALL | Logical language: Logical universal quantifier. |
| FORMAL_PROOF | A formal proof. |
| FORMULA | Logical language: Formula. |
| FORMULATYPE | Type for a formula. |
| FUNCON | Logical language: Function constant. |
| FUNVAR | Logical language: Function variable. |
| IMPL | Logical language: Logical implication. |
| L | A proofline that derives from previous derived formulas. |
| LATEX | For each supported language entry one can find a LaTeX text here. |
| LINES | List of proof lines. |
| LINETYPE | Type for a proof line of a formal proof. |
| MP | The rule Modus Ponens (or for short MP) is the sole rule of inference in propositional calculus. |
| NODE | This part is the smallest unit and corresponds to the LaTeX item subsection. |
| NODE.NAME | Short text to describe this item. |
| NODE.SUCCEEDING | |
| NODETYPE | Type for a node. |
| NOT | Logical language: Logical negation. |
| OR | Logical language: Logical disjunction. |
| PRECEDING | Text that precedes the mathematical meat. |
| PREDCON | Logical language: Predicate constant. |
| PREDVAR | Logical language: Predicate variable. |
| PROOF | An informal proof. |
| QEDEQ | Root element. |
| QEDEQ.BIBLIOGRAPHY | Literature references. |
| QEDEQ.BIBLIOGRAPHY.ITEM | Single literature reference. |
| QEDEQ.CHAPTER | This part corresponds to the LaTeX item chapter. |
| QEDEQ.CHAPTER.INTRODUCTION | Chapter contents description. |
| QEDEQ.CHAPTER.SECTION | Section of chapter. |
| QEDEQ.CHAPTER.SECTION.INTRODUCTION | Section contents description. |
| QEDEQ.CHAPTER.SECTION.SUBSECTIONS | List of subsections. |
| QEDEQ.HEADER | File specification, information about the authors, imports of other QEDEQ modules and so on are part of the header. |
| QEDEQ.HEADER.ABSTRACT | Module contents description. |
| QEDEQ.HEADER.AUTHORS | List of authors of this module. |
| QEDEQ.HEADER.AUTHORS.AUTHOR | Name and email address of author. |
| QEDEQ.HEADER.AUTHORS.AUTHOR.NAME | Name of author. |
| QEDEQ.HEADER.IMPORTS | References to other QEDEQ modules that are a precondition for this one. |
| QEDEQ.HEADER.IMPORTS.IMPORT | A single reference to a QEDEQ module that must be imported. |
| QEDEQ.HEADER.USEDBY | List of QEDEQ modules which use (import) this module. |
| QUANTIFIER_INTERSECTION | Logical language: Intersection about all classes that fullfil a property. |
| QUANTIFIER_UNION | Logical language: Union about all classes that fullfil a property. |
| REASONTYPE | Type for a rule that can derive a new formula. |
| RENAME | Rename of bound subject variable at given occurrence by another one. |
| RULE | A new meta rule. |
| RULE.CHANGED_RULE | Modifications to other existing rules. |
| RULE.DESCRIPTION | Additional description. |
| RULE.LINK | References to theorems or axioms. |
| RULE.PROOF | Informal proof for this rule. |
| SPECIFICATION | File specification of this module. |
| SPECIFICATION.LOCATIONS | List of locations to find the QEDEQ module. |
| SPECIFICATION.LOCATIONS.LOCATION | Location of a QEDEQ module. |
| SUBSECTION | This a normal LaTeX subsection of a section. |
| SUBSECTION.TEXT | The LaTeX text of this subsection. |
| SUBSECTIONTYPE | Type for a subsection. |
| SUBST_FREE | Substitute of free subject variable by term. |
| SUBST_FUNVAR | Substitute of function variable by term. |
| SUBST_PREDVAR | Substitute of predicate variable by formula. |
| SUCCEEDING | Text that succeeds mathematical meat. |
| TERM | Logical language: Term. |
| TERMTYPE | Type for a term. |
| THEOREM | A theorem and it's proof. |
| THEOREM.DESCRIPTION | Additional description. |
| TITLE | Title of a text segment. |
| UNIVERSAL | Rule of universal generalization. |
| VAR | Logical language: Subject variable. |
| Simple Type Summary | |
| EMAILTYPE | Type for an email. |
| LEVELTYPE | Type for a level. |
| LOCATIONTYPE | Type for a location. |
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" - http://www.qedeq.org
Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
| |||||||
| DETAILS: DOCUMENTATION | | FRAMES | NO FRAMES | ||||||