Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| Hilbert II - JAVA-Packages - Principia Mathematica II
PREV NEXT | FRAMES NO FRAMES

## Uses of Interface
com.meyling.principia.logic.basic.Formula

Packages that use Formula
com.meyling.principia.logic.basic |
com.meyling.principia.logic.rule |
com.meyling.principia.module |

Uses of Formula in com.meyling.principia.logic.basic

Classes in com.meyling.principia.logic.basic that implement Formula
`class` | `AbstractFormula` From this abstract implementation of Formula each non abstract Formula must inherit from.
`class` | `BasicFormulaPatternVariable` Pattern variable, for matching purposes.
`class` | `BasicPredicateVariablePatternVariable` Pattern variable, for matching purposes.
`class` | `Conjunction` Conjunction of formulas.
`class` | `Disjunction` Disjunction of formulas.
`class` | `Equivalence` Equivalence of formulas.
`class` | `ExistentialQuantifier` Existential quantifier, logical "exists".
`class` | `Implication` Implication of formulas.
`class` | `LogicalOperatorWithTwoFormulas` LogicalOperatorWithTwoFormulas of formulas.
`class` | `Negation` Logical negation, logical "not".
`class` | `PredicateVariable` Predicate variable with argument list.
`class` | `PropositionVariable` Represents an arbitrary logical proposition.
`class` | `Quantifier` Basis class for Quantifier.
`class` | `UniversalQuantifier` Universal qualifier, logical "for all".

Methods in com.meyling.principia.logic.basic that return Formula
`Formula` | `Formula.getPartFormula(int i)` Get the requested part formula
`Formula` | `Formula.replaceBoundSubjectVariable(Enumerator counter, int occurrence, SubjectVariable search, SubjectVariable replacement)` Replace the `occurrence`-th occurence of a bound `SubjectVariable` by another one.
`Formula` | `Formula.replaceBoundSubjectVariables(Enumerator counter)` Replace every bound SubjectVariable by a BasicSubjectVariablePatternVariable
`Formula` | `BasicFormulaPatternVariable.getPartFormula(int i)`
`Formula` | `BasicFormulaPatternVariable.replaceBoundSubjectVariable(Enumerator counter, int occurance, SubjectVariable search, SubjectVariable replacement)`
`Formula` | `BasicFormulaPatternVariable.replaceBoundSubjectVariables(Enumerator counter)`
`Formula` | `Quantifier.getPartFormula(int i)`
`Formula` | `PropositionVariable.getPartFormula(int i)`
`Formula` | `BasicPredicateVariablePatternVariable.getPartFormula(int i)`
`Formula` | `BasicPredicateVariablePatternVariable.replaceBoundSubjectVariable(Enumerator counter, int occurance, SubjectVariable search, SubjectVariable replacement)`
`Formula` | `BasicPredicateVariablePatternVariable.replaceBoundSubjectVariables(Enumerator counter)`
`Formula` | `LogicalOperatorWithTwoFormulas.getPartFormula(int i)`
`static Formula` | `AbstractFormula.createPattern(Formula formula)` Replace the every occurence of a `SubjectVariable` by a `BasicSubjectVariablePatternVariable`, every `PropositionVariable` by a `BasicFormulaPatternVariable` and TODO not yet: every `PredicateVariable` by a `BasicPredicateVariablePatternVariable`.
`abstract Formula` | `AbstractFormula.getPartFormula(int i)`
`Formula` | `AbstractFormula.replaceBoundSubjectVariable(Enumerator counter, int occurance, SubjectVariable search, SubjectVariable replacement)`
`Formula` | `AbstractFormula.replaceBoundSubjectVariables(Enumerator counter)`
`Formula` | `PredicateVariable.getPartFormula(int i)`
`Formula` | `Negation.getPartFormula(int i)`

Methods in com.meyling.principia.logic.basic with parameters of type Formula
`static Formula` | `AbstractFormula.createPattern(Formula formula)` Replace the every occurence of a `SubjectVariable` by a `BasicSubjectVariablePatternVariable`, every `PropositionVariable` by a `BasicFormulaPatternVariable` and TODO not yet: every `PredicateVariable` by a `BasicPredicateVariablePatternVariable`.

Constructors in com.meyling.principia.logic.basic with parameters of type Formula
`LogicalOperatorWithTwoFormulas(Formula formula1, Formula formula2)` Constructs a new formula out of two given ones.
`Disjunction(Formula formula1, Formula formula2)` Constructs a logical disjunction.
`Implication(Formula formula1, Formula formula2)` Constructs a logical implication.
`Negation(Formula formula)` Constructs negation of formula.
`Equivalence(Formula formula1, Formula formula2)` Constructs a logical equivalence.
`Conjunction(Formula formula1, Formula formula2)` Constructs a logical conjunction.

Uses of Formula in com.meyling.principia.logic.rule

Methods in com.meyling.principia.logic.rule with parameters of type Formula
`void` | `LeftAdditionConjunction.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of left addition of a conjunction.
`void` | `RenameFreeSubjectVariable.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula by replacing a free subject variable of a proof line by another subject variable.
`void` | `ConjunctionRule.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of conjunction rule.
`void` | `SubstLine.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with `formula`.
`void` | `ReplacePropositionVariable.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula if the proposition variable is replaced by the formula of the constructor.
`void` | `ReverseImplication.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of reversing an implication.
`void` | `Rule.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula (using the arguments of rule).
`void` | `RightAddition.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of right addition.
`void` | `AddSentence.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula.
`void` | `LeftAddition.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of left addition.
`void` | `RightAdditionImplication.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of right addition of a implication.
`void` | `LeftAdditionImplication.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of right addition of a implication.
`void` | `ReplacePredicateVariable.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula if replacing the predicate variable by the formula of the constructor.
`void` | `RenameBoundSubjectVariable.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula by replacing a bound subject variable of a proof line by another subject variable at a certain occurance.
`void` | `AddAxiom.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with `formula`.
`void` | `Generalization.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of modus ponens.
`void` | `Particularization.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with a formula because of modus ponens.
`void` | `ApplySentence.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with `formula`.
`void` | `ApplyAxiom.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with `formula`.
`void` | `HypotheticalSyllogism.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of hypothetical syllogism.
`void` | `ReverseAbbreviation.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula.
`void` | `ElementaryEquivalence.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula.
`void` | `UseAbbreviation.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula.
`void` | `RightAdditionEquivalence.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of right addition of a implication.
`void` | `LeftAdditionEquivalence.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of right addition of a implication.
`void` | `ModusPonens.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of modus ponens.
`void` | `RightAdditionConjunction.check(Module module, ProofLineList proofLines, int position, Formula formula)` Check if proof could be extended with formula because of right addition of a conjunction.

Uses of Formula in com.meyling.principia.module

Methods in com.meyling.principia.module that return Formula
`Formula` | `Module.getLabeledFormula(String label)` Get the sentence or axiom formula with label `label`.

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| Hilbert II - JAVA-Packages - Principia Mathematica II
PREV NEXT | FRAMES NO FRAMES

©left GNU General Public Licence All Rights Reserved.