# Project "Principia" # # Michael Meyling # Stoltenstrasse 38 # 22119 Hamburg # Germany # # @version $Revision: 0.00.51$ # @author Michael Meyling # Rule Overview Version 1.00.00 Class Description AddAxiom add previous axiom to proof lines AddSentence add previous proposition to proof lines Generalization generalize a formula ModusPonens use modus ponens Particularization particularize a formula RenameBoundSubjectVariable rename a bound variable RenameFreeSubjectVariable rename a free variable ReplacePredicateVariable replace predicate variable ReplacePropositionVariable replace proposition variable by formula UseAbbreviation use previous abbreviation ReverseAbbreviation unuse previous abbreviation Version 1.01.00 Class Description SubstLine substitute various variables of a proof line Version 1.01.01 Class Description ApplyAxiom add axiom, substitute, use modus ponens ApplySentence add proposition, subsitute, use modus ponens Version 1.01.02 Class Description HypotheticalSyllogism use hypothetical syllogism Version 1.01.03 Class Description RightAddition right addition of disjunction to implication Version 1.01.04 Class Description LeftAddition left addition of disjunction to implication ReverseImplication build correct reversion of an implication Version 1.01.05 Class Description LeftAdditionConjunction left addition of conjunction to implication RightAdditionConjunction right addition of conjunction to implication LeftAdditionImplication left addition of implication to implication RightAdditionImplication right addition of implication to implication Version 1.01.06 Class Description LeftAdditionEquivalence left addition of equivalence to implication RightAdditionEquivalence right addition of equivalence to implication Version 1.02.00 Class Description ElementaryEquivalence if two formulas impies each other any occurence of one formula could be replaced by the other one Version 1.02.01 Class Description ConjunctionRule conjunction of two proofed formulas