Orbital library

Uses of Interface
orbital.logic.imp.Formula

Packages that use Formula
orbital.logic.imp Defines a generic interface to (symbolic) logic systems. 
orbital.moon.logic Contains implementations of some logics as well as a logic and mathematical expression parser. 
orbital.moon.logic.resolution Provides resolution inference theorem prover implementation and clause management. 
 

Uses of Formula in orbital.logic.imp
 

Subinterfaces of Formula in orbital.logic.imp
static interface Formula.Composite
          Interface for composite formulas.
 

Classes in orbital.logic.imp that implement Formula
 class LogicBasis
          This abstract LogicBasis class derives the extended logic operations depending upon basic logic operations.
 

Methods in orbital.logic.imp that return Formula
 Formula Formula.and(Formula B)
          Conjunction and: FG.
 Formula LogicBasis.equiv(Formula B)
          Equivalence equiv: A ⇔ B is calced (A→B) ∧ (B→A)
 Formula Formula.equiv(Formula B)
          Equivalence equiv: FG.
 Formula LogicBasis.exists(Symbol x)
          Existence-quantifier exists: x A is calced ¬∀x ¬A.
 Formula Formula.exists(Symbol x)
          Existential-quantifier exists: ∃x F.
 Formula LogicBasis.forall(Symbol x)
          All-quantifier forall: x A is calced ¬∃x ¬A.
 Formula Formula.forall(Symbol x)
          Universal-quantifier forall: ∀x F.
 Formula LogicBasis.impl(Formula B)
          Implication impl: A → B is calced ¬A ∨ B
 Formula Formula.impl(Formula B)
          Implication impl: FG.
 Formula Formula.not()
          Negation not: ¬F.
 Formula Formula.or(Formula B)
          Disjunction or: FG.
 Formula LogicBasis.xor(Formula B)
          Exclusion xor: A xor B is calced (A∧¬B) ∨ (¬A∧B)
 Formula Formula.xor(Formula B)
          Exclusion xor: F ∨̇ G = F xor G.
 

Methods in orbital.logic.imp with parameters of type Formula
 Formula Formula.and(Formula B)
          Conjunction and: FG.
 Formula LogicBasis.equiv(Formula B)
          Equivalence equiv: A ⇔ B is calced (A→B) ∧ (B→A)
 Formula Formula.equiv(Formula B)
          Equivalence equiv: FG.
 Formula LogicBasis.impl(Formula B)
          Implication impl: A → B is calced ¬A ∨ B
 Formula Formula.impl(Formula B)
          Implication impl: FG.
 boolean Inference.infer(Formula[] w, Formula d)
          Apply the inference relation |~ according to the implementation calculus K.
 boolean Inference.infer(Formula[] w, Formula d)
          Apply the inference relation |~ according to the implementation calculus K.
 Formula Formula.or(Formula B)
          Disjunction or: FG.
 boolean Logic.satisfy(Interpretation I, Formula F)
          Defines the semantic satisfaction relation ⊧.
 Formula LogicBasis.xor(Formula B)
          Exclusion xor: A xor B is calced (A∧¬B) ∨ (¬A∧B)
 Formula Formula.xor(Formula B)
          Exclusion xor: F ∨̇ G = F xor G.
 

Uses of Formula in orbital.moon.logic
 

Methods in orbital.moon.logic that return Formula
static Formula ClassicalLogic.Utilities.conjunctiveForm(Formula f)
          Transforms into conjunctive normal form (CNF).
static Formula ClassicalLogic.Utilities.conjunctiveForm(Formula f, boolean simplifying)
          Transforms into conjunctive normal form (CNF).
static Formula ClassicalLogic.Utilities.constantClosure(Formula F)
          Get the constant-closure of a formula.
 Formula ClassicalLogic.createFormula(java.lang.String expression)
          Deprecated. Use (Formula) createExpression(expression) instead.
static Formula ClassicalLogic.Utilities.disjunctiveForm(Formula f)
          Transforms into disjunctive normal form (DNF).
static Formula ClassicalLogic.Utilities.disjunctiveForm(Formula f, boolean simplifying)
          Transforms into disjunctive normal form (DNF).
static Formula ClassicalLogic.Utilities.dropQuantifiers(Formula F)
          Drop any quantifiers.
static Formula ClassicalLogic.Utilities.existentialClosure(Formula F)
          Get the ∃-closure of a formula.
static Formula ClassicalLogic.Utilities.negation(Formula F)
          Get the negation of F without introducing duplex negatios.
static Formula ClassicalLogic.Utilities.negationForm(Formula F)
          Get the negation normal form of a formula.
static Formula ClassicalLogic.Utilities.skolemForm(Formula F)
          Get the Skolem normal form of a formula.
static Formula ClassicalLogic.Utilities.universalClosure(Formula F)
          Get the ∀-closure of a formula.
 

Methods in orbital.moon.logic with parameters of type Formula
static java.util.Set ClassicalLogic.Utilities.clausalForm(Formula f, boolean simplifying)
          Deprecated. Prefer to use the more general method ClausalFactory.asClausalSet(orbital.logic.imp.Formula) instead.
static Formula ClassicalLogic.Utilities.conjunctiveForm(Formula f)
          Transforms into conjunctive normal form (CNF).
static Formula ClassicalLogic.Utilities.conjunctiveForm(Formula f, boolean simplifying)
          Transforms into conjunctive normal form (CNF).
static Formula ClassicalLogic.Utilities.constantClosure(Formula F)
          Get the constant-closure of a formula.
static Formula ClassicalLogic.Utilities.disjunctiveForm(Formula f)
          Transforms into disjunctive normal form (DNF).
static Formula ClassicalLogic.Utilities.disjunctiveForm(Formula f, boolean simplifying)
          Transforms into disjunctive normal form (DNF).
static Formula ClassicalLogic.Utilities.dropQuantifiers(Formula F)
          Drop any quantifiers.
static Formula ClassicalLogic.Utilities.existentialClosure(Formula F)
          Get the ∃-closure of a formula.
static Formula ClassicalLogic.Utilities.negation(Formula F)
          Get the negation of F without introducing duplex negatios.
static Formula ClassicalLogic.Utilities.negationForm(Formula F)
          Get the negation normal form of a formula.
 boolean ModalLogic.satisfy(Interpretation I, Formula F)
           
 boolean FuzzyLogic.satisfy(Interpretation I, Formula F)
           
 boolean ClassicalLogic.satisfy(Interpretation I, Formula F)
           
static Formula ClassicalLogic.Utilities.skolemForm(Formula F)
          Get the Skolem normal form of a formula.
static Formula ClassicalLogic.Utilities.universalClosure(Formula F)
          Get the ∀-closure of a formula.
 

Uses of Formula in orbital.moon.logic.resolution
 

Methods in orbital.moon.logic.resolution that return Formula
 Formula ClauseImpl.toFormula()
           
 Formula Clause.toFormula()
          Convert this clause to a formula representation.
 Formula ClausalSetImpl.toFormula()
           
 Formula ClausalSet.toFormula()
          Convert this set of clauses to a formula representation.
 

Methods in orbital.moon.logic.resolution with parameters of type Formula
 ClausalSet DefaultClausalFactory.asClausalSet(Formula f)
           
 ClausalSet ClausalFactory.asClausalSet(Formula formula)
          Returns a clausal set representation of the given formula.
 java.util.Iterator ClausalIndex.getProbableComplementClauses(Formula L)
          Get an iterator of all clauses that contain literals which could possibly unify with ~L.
 java.util.Iterator ClausalIndex.getProbableComplementLiterals(Formula L)
          Get an iterator of all literals which could possibly unify with ~L.
 java.util.Iterator ClausalIndex.getProbableComplements(Formula L)
          Get an iterator of all (clause,literal) pairs which could possibly unify with ~L.
 java.util.Iterator ClausalIndex.getProbableUnifiableClauses(Formula L)
          Get an iterator of all clauses that contain literals which could possibly unify with L.
 java.util.Iterator ClausalIndex.getProbableUnifiableLiterals(Formula L)
          Get an iterator of all literals which could possibly unify with L.
 java.util.Iterator OrderedClauseImpl.getProbableUnifiables(Formula L)
           
 java.util.Iterator IndexedClauseImpl.getProbableUnifiables(Formula L)
           
 java.util.Iterator IndexedClausalSetImpl.getProbableUnifiables(Formula L)
          Get an iterator of all clauses that contain literals which could possibly unify with L.
 java.util.Iterator ClauseImpl.getProbableUnifiables(Formula L)
           
 java.util.Iterator Clause.getProbableUnifiables(Formula L)
          Get (an iterator over) all literals contained in this clause that may possibly unify with L.
 java.util.Iterator ClausalIndex.getProbableUnifiables(Formula L)
          Get an iterator of all (clause,literal) pairs which could possibly unify with L.
 java.util.Set ClauseImpl.getUnifiables(Formula L)
           
 java.util.Set Clause.getUnifiables(Formula L)
          Get all literals contained in this clause that unify with L.
 boolean ResolutionBase.infer(Formula[] B, Formula D)
          Apply the inference relation |~ according to the implementation calculus K.
 boolean ResolutionBase.infer(Formula[] B, Formula D)
          Apply the inference relation |~ according to the implementation calculus K.
protected  Clause OrderedClauseImpl.resolventWith(Clause _G, Formula L, Formula K)
           
protected  Clause ClauseImpl.resolventWith(Clause G, Formula L, Formula K)
          Resolve clause F with G by the complementary resolution literals L∈F and K∈G.
protected  Pair ClauseImpl.resolventWith2(Clause G, Formula L, Formula K)
          Workaround for returning 2 arguments.
 


Orbital library
1.3.0: 11 Apr 2009

Copyright © 1996-2009 André Platzer
All Rights Reserved.