Modifier and Type | Method and Description |
---|---|
private java.util.Set<PropositionalFormula> |
SActionQuerySatisfactionTester.getQueryParts(PropositionalFormula formula)
Calculates the set of all subformulas of an action query down to
propositions (holds, always, necessarily)
|
Modifier and Type | Method and Description |
---|---|
private java.lang.String |
SActionQuerySatisfactionTester.getQueryPartRules(PropositionalFormula queryPart)
Calculates the translation of an action query to rules of a normal logic
program according to the translation sheme presented in [1].
|
private java.util.Set<PropositionalFormula> |
SActionQuerySatisfactionTester.getQueryParts(PropositionalFormula formula)
Calculates the set of all subformulas of an action query down to
propositions (holds, always, necessarily)
|
Modifier and Type | Method and Description |
---|---|
private PropositionalFormula |
ActionQueryParser.parseAtomic(java.util.List<java.lang.Object> l)
Parses a simple formula as a list of String tokens or formulas into a propositional formula.
|
private PropositionalFormula |
ActionQueryParser.parseConjunction(java.util.List<java.lang.Object> l)
Parses a simple formula as a list of String tokens or formulas into a propositional formula.
|
private PropositionalFormula |
ActionQueryParser.parseDisjunction(java.util.List<java.lang.Object> l)
Parses a simple formula as a list of String tokens or formulas into a propositional formula.
|
private PropositionalFormula |
ActionQueryParser.parseNegation(java.util.List<java.lang.Object> l)
Parses a simple formula as a list of String tokens or formulas into a propositional formula.
|
Modifier and Type | Class and Description |
---|---|
class |
AlwaysQuery
This class represents an always query in the action query language S.
|
class |
HoldsQuery
This class represents a holds query in the action query language S.
|
class |
NecessarilyQuery
This class represents a necessarily query in the action query language S.
|
class |
QueryProposition
Action queries are represented as propositional formulas with three possible
types of propositions: holds, always and necessarily propositions.
|
Modifier and Type | Field and Description |
---|---|
protected PropositionalFormula |
SActionQuery.formula |
Modifier and Type | Method and Description |
---|---|
PropositionalFormula |
SActionQuery.getFormula()
Returns the formula represented by this action query.
|
private static PropositionalFormula |
SActionQuery.substitutePropositions(java.util.Map<Variable,Constant> map,
PropositionalFormula formula)
Utility function that walks through all parts of a propositional formula
with query propositions substituting all variables with constants according
to the given map.
|
Modifier and Type | Method and Description |
---|---|
private static PropositionalFormula |
SActionQuery.substitutePropositions(java.util.Map<Variable,Constant> map,
PropositionalFormula formula)
Utility function that walks through all parts of a propositional formula
with query propositions substituting all variables with constants according
to the given map.
|
Constructor and Description |
---|
SActionQuery(PropositionalFormula formula)
Creates a new action query with the given propositional formula and no
grounding requirements.
|
SActionQuery(PropositionalFormula formula,
java.util.Set<GroundingRequirement> requirements)
Creates a new action query with the given propositional formula
and grounding requirements.
|
Constructor and Description |
---|
ExecutableFormulaSet(java.util.Collection<? extends PropositionalFormula> formulas)
Creates a new set for the given formulas.
|
Modifier and Type | Field and Description |
---|---|
private DialogueTrace<PropositionalFormula,java.util.Collection<PropositionalFormula>> |
DeductiveEnvironment.trace
The current dialogue trace.
|
private DialogueTrace<PropositionalFormula,java.util.Collection<PropositionalFormula>> |
DeductiveEnvironment.trace
The current dialogue trace.
|
Modifier and Type | Method and Description |
---|---|
DialogueTrace<PropositionalFormula,java.util.Collection<PropositionalFormula>> |
DeductiveEnvironment.getDialogueTrace()
Returns the current dialogue trace.
|
DialogueTrace<PropositionalFormula,java.util.Collection<PropositionalFormula>> |
DeductiveEnvironment.getDialogueTrace()
Returns the current dialogue trace.
|
Modifier and Type | Method and Description |
---|---|
PropositionalFormula |
PlFormulaGenerator.getRuleFormula(DefeasibleInferenceRule<PropositionalFormula> r) |
Modifier and Type | Method and Description |
---|---|
PropositionalFormula |
PlFormulaGenerator.getRuleFormula(DefeasibleInferenceRule<PropositionalFormula> r) |
Modifier and Type | Method and Description |
---|---|
static AspicArgumentationTheory<PropositionalFormula> |
RandomAspicArgumentationTheoryGenerator.next(int numPropositions,
int numFormulas,
int maxBodyLiterals,
double probStrict)
Generates a random ASPIC argumentation theory with
numPropositions
and numFormulas formulas (inference rules). |
Modifier and Type | Method and Description |
---|---|
java.lang.Double |
AbstractDeductiveArgumentationReasoner.query(DeductiveKnowledgeBase kb,
PropositionalFormula f) |
Modifier and Type | Method and Description |
---|---|
private ArgumentTree |
SimpleReasoner.getArgumentTree(DeductiveKnowledgeBase kb,
DeductiveArgumentNode argNode,
java.util.Set<PropositionalFormula> support)
Computes the argument tree of the given argument.
|
Modifier and Type | Field and Description |
---|---|
private PropositionalFormula |
DeductiveArgument.claim
The claim of this argument.
|
Modifier and Type | Field and Description |
---|---|
private java.util.Collection<? extends PropositionalFormula> |
DeductiveArgument.support
The support of this argument.
|
Modifier and Type | Method and Description |
---|---|
PropositionalFormula |
DeductiveArgument.getClaim()
Returns the claim of this argument.
|
Modifier and Type | Method and Description |
---|---|
java.util.Collection<? extends PropositionalFormula> |
DeductiveArgument.getSupport()
Returns the support of this argument.
|
Modifier and Type | Method and Description |
---|---|
private void |
Compilation.subcuts(DeductiveArgumentNode argNode,
java.util.Set<CompilationNode> remainingNodes,
CompilationNode current,
java.util.Set<PropositionalFormula> currentSupport,
ArgumentTree argTree)
This method recursively builds up the argument tree from
the given argument.
|
Constructor and Description |
---|
DeductiveArgument(java.util.Collection<? extends PropositionalFormula> support,
PropositionalFormula claim)
Creates a new deductive argument with the given support
and claim.
|
DeductiveArgumentNode(java.util.Collection<? extends PropositionalFormula> support,
PropositionalFormula claim)
Creates a new deductive argument node with the given support
and claim (a unique ID is generated)
|
Constructor and Description |
---|
CompilationNode(java.util.Collection<? extends PropositionalFormula> formulas)
Creates a new compilation node with the given
set of formulas.
|
DeductiveArgument(java.util.Collection<? extends PropositionalFormula> support,
PropositionalFormula claim)
Creates a new deductive argument with the given support
and claim.
|
DeductiveArgumentNode(java.util.Collection<? extends PropositionalFormula> support,
PropositionalFormula claim)
Creates a new deductive argument node with the given support
and claim (a unique ID is generated)
|
Modifier and Type | Field and Description |
---|---|
private PropositionalFormula |
SimplePlLogicArgument.claim |
private PropositionalFormula |
SimplePlRule.claim |
Modifier and Type | Field and Description |
---|---|
private java.util.Set<PropositionalFormula> |
SimplePlRule.support |
Modifier and Type | Method and Description |
---|---|
PropositionalFormula |
SimplePlLogicArgument.getClaim() |
PropositionalFormula |
SimplePlRule.getConclusion() |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<? extends PropositionalFormula> |
SimplePlRule.getPremise() |
Modifier and Type | Method and Description |
---|---|
void |
SimplePlRule.addPremise(PropositionalFormula arg0) |
java.util.Set<DeductiveArgument> |
DeductiveKnowledgeBase.getDeductiveArguments(PropositionalFormula claim)
Computes all deductive arguments for the given claim.
|
void |
SimplePlRule.setConclusion(PropositionalFormula arg0) |
Modifier and Type | Method and Description |
---|---|
void |
SimplePlRule.addPremises(java.util.Collection<? extends PropositionalFormula> arg0) |
Constructor and Description |
---|
SimplePlLogicArgument(java.util.Collection<SimplePlRule> _support,
PropositionalFormula _claim) |
SimplePlRule(PropositionalFormula _claim) |
SimplePlRule(PropositionalFormula _claim,
java.util.Set<PropositionalFormula> _support) |
Constructor and Description |
---|
DeductiveKnowledgeBase(java.util.Collection<? extends PropositionalFormula> formulas)
Creates a new knowledge base with the given
set of formulas.
|
SimplePlRule(PropositionalFormula _claim,
java.util.Set<PropositionalFormula> _support) |
Modifier and Type | Field and Description |
---|---|
private java.util.Collection<InformationObject<PropositionalFormula>> |
AbstractCredibilityComparer.formulas
The information objects that hold the information which agents
uttered the formulas.
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
AbstractCredibilityComparer.isAtLeastAsPreferredAs(PropositionalFormula f,
java.util.Collection<? extends PropositionalFormula> formulas)
Checks whether f is at least as preferred as some formula in "formulas"
|
protected boolean |
AbstractCredibilityComparer.isAtLeastAsPreferredAs(PropositionalFormula f,
PropositionalFormula f2)
Checks whether f is at least as preferred as f2
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
AbstractCredibilityComparer.isAtLeastAsPreferredAs(java.util.Collection<? extends PropositionalFormula> col1,
java.util.Collection<? extends PropositionalFormula> col2)
Checks whether col1 is at least as preferred as col2 wrt.
|
protected boolean |
AbstractCredibilityComparer.isAtLeastAsPreferredAs(java.util.Collection<? extends PropositionalFormula> col1,
java.util.Collection<? extends PropositionalFormula> col2)
Checks whether col1 is at least as preferred as col2 wrt.
|
protected boolean |
AbstractCredibilityComparer.isAtLeastAsPreferredAs(PropositionalFormula f,
java.util.Collection<? extends PropositionalFormula> formulas)
Checks whether f is at least as preferred as some formula in "formulas"
|
Constructor and Description |
---|
AbstractCredibilityComparer(java.util.Collection<InformationObject<PropositionalFormula>> formulas,
Order<Agent> credOrder)
Creates a new credibility comparer that is guided by the giving information which
agents uttered the formulas and the credibility order.
|
CredibilityCategorizer(java.util.Collection<InformationObject<PropositionalFormula>> formulas,
Order<Agent> credOrder)
Creates a new credibility categorizer that is guided by the giving information which
agents uttered the formulas and the credibility order.
|
Modifier and Type | Method and Description |
---|---|
java.util.Collection<InformationObject<PropositionalFormula>> |
CrMasSimpleRevisionOperator.revise(java.util.Collection<InformationObject<PropositionalFormula>> base,
java.util.Collection<InformationObject<PropositionalFormula>> formulas) |
java.util.Collection<InformationObject<PropositionalFormula>> |
CrMasArgumentativeRevisionOperator.revise(java.util.Collection<InformationObject<PropositionalFormula>> base,
java.util.Collection<InformationObject<PropositionalFormula>> formulas) |
java.util.Collection<PropositionalFormula> |
ArgumentativeRevisionOperator.revise(java.util.Collection<PropositionalFormula> base,
java.util.Collection<PropositionalFormula> formulas) |
Modifier and Type | Method and Description |
---|---|
boolean |
CrMasSimpleRevisionOperator.CredibilityComparer.isFormerAtLeastAsPreferredAsLatter(PropositionalFormula f,
java.util.Collection<PropositionalFormula> formulas) |
Modifier and Type | Method and Description |
---|---|
boolean |
CrMasSimpleRevisionOperator.CredibilityComparer.isFormerAtLeastAsPreferredAsLatter(PropositionalFormula f,
java.util.Collection<PropositionalFormula> formulas) |
java.util.Collection<InformationObject<PropositionalFormula>> |
CrMasSimpleRevisionOperator.revise(java.util.Collection<InformationObject<PropositionalFormula>> base,
java.util.Collection<InformationObject<PropositionalFormula>> formulas) |
java.util.Collection<InformationObject<PropositionalFormula>> |
CrMasSimpleRevisionOperator.revise(java.util.Collection<InformationObject<PropositionalFormula>> base,
java.util.Collection<InformationObject<PropositionalFormula>> formulas) |
java.util.Collection<InformationObject<PropositionalFormula>> |
CrMasArgumentativeRevisionOperator.revise(java.util.Collection<InformationObject<PropositionalFormula>> base,
java.util.Collection<InformationObject<PropositionalFormula>> formulas) |
java.util.Collection<InformationObject<PropositionalFormula>> |
CrMasArgumentativeRevisionOperator.revise(java.util.Collection<InformationObject<PropositionalFormula>> base,
java.util.Collection<InformationObject<PropositionalFormula>> formulas) |
java.util.Collection<PropositionalFormula> |
ArgumentativeRevisionOperator.revise(java.util.Collection<PropositionalFormula> base,
java.util.Collection<PropositionalFormula> formulas) |
java.util.Collection<PropositionalFormula> |
ArgumentativeRevisionOperator.revise(java.util.Collection<PropositionalFormula> base,
java.util.Collection<PropositionalFormula> formulas) |
Constructor and Description |
---|
CredibilityComparer(java.util.Collection<InformationObject<PropositionalFormula>> formulas,
Order<Agent> credOrder) |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<PropositionalFormula> |
ArgumentativeTransformationFunction.transform(java.util.Collection<PropositionalFormula> formulas) |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<PropositionalFormula> |
ArgumentativeTransformationFunction.transform(java.util.Collection<PropositionalFormula> formulas) |
Modifier and Type | Method and Description |
---|---|
java.lang.Boolean |
AbstractConditionalLogicReasoner.query(ClBeliefSet beliefbase,
PropositionalFormula formula) |
Modifier and Type | Method and Description |
---|---|
private void |
BruteForceCReasoner.filter(java.util.ArrayList<PropositionalFormula> list,
ClBeliefSet beliefset) |
Modifier and Type | Method and Description |
---|---|
java.lang.Integer |
RankingFunction.rank(PropositionalFormula formula)
Gets the rank of the given formula.
|
Modifier and Type | Method and Description |
---|---|
void |
RankingFunction.forceStrictness(java.util.Set<PropositionalFormula> formulas)
Sets the rank of every interpretation i that does not satisfy
the given set of formulas to RankingFunction.INFINITY.
|
Modifier and Type | Field and Description |
---|---|
private PropositionalFormula |
Conditional.conclusion
The conclusion of this conditional.
|
private PropositionalFormula |
Conditional.premise
The premise of this conditional.
|
Modifier and Type | Method and Description |
---|---|
PropositionalFormula |
Conditional.getConclusion() |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<PropositionalFormula> |
Conditional.getPremise() |
Modifier and Type | Method and Description |
---|---|
void |
Conditional.addPremise(PropositionalFormula premise) |
void |
Conditional.setConclusion(PropositionalFormula conclusion) |
Modifier and Type | Method and Description |
---|---|
void |
Conditional.addPremises(java.util.Collection<? extends PropositionalFormula> premises) |
Constructor and Description |
---|
Conditional(PropositionalFormula conclusion)
Creates a new conditional with a tautological premise
and given conclusion.
|
Conditional(PropositionalFormula premise,
PropositionalFormula conclusion)
Creates a new conditional with the given premise
and conclusion.
|
Modifier and Type | Method and Description |
---|---|
abstract java.lang.Double |
AbstractPclReasoner.query(PclBeliefSet beliefbase,
PropositionalFormula formula) |
java.lang.Double |
DefaultMeReasoner.query(PclBeliefSet beliefbase,
PropositionalFormula formula) |
java.lang.Double |
GeneralizedMeReasoner.query(PclBeliefSet beliefbase,
PropositionalFormula formula) |
Modifier and Type | Class and Description |
---|---|
class |
ProbabilityDistribution<T extends Interpretation<PlBeliefSet,PropositionalFormula>>
This class represents a probability distribution on some logical language
|
Modifier and Type | Method and Description |
---|---|
static <S extends Interpretation<PlBeliefSet,PropositionalFormula>> |
ProbabilityDistribution.convexCombination(double[] factors,
ProbabilityDistribution<S>[] creators)
Computes the convex combination of the
given probability distributions P1,...,PN with parameters factors, i.e.
|
static <S extends Interpretation<PlBeliefSet,PropositionalFormula>> |
ProbabilityDistribution.getUniformDistribution(java.util.Set<S> interpretations,
Signature sig)
Returns the uniform distribution on the given interpretations.
|
Modifier and Type | Method and Description |
---|---|
Probability |
ProbabilityDistribution.probability(PropositionalFormula f)
Returns the probability of the given formula
|
Modifier and Type | Method and Description |
---|---|
Probability |
ProbabilityDistribution.probability(Interpretation<PlBeliefSet,PropositionalFormula> w)
Gets the probability of the given Herbrand interpretation (this is just an
alias for get(Object o).
|
Constructor and Description |
---|
ProbabilisticConditional(PropositionalFormula conclusion,
Probability probability)
Creates a new probabilistic conditional with a tautological premise
and given conclusion and probability.
|
ProbabilisticConditional(PropositionalFormula premise,
PropositionalFormula conclusion,
Probability probability)
Creates a new probabilistic conditional with the given premise,
conclusion, and probability.
|
Modifier and Type | Field and Description |
---|---|
private ConsistencyWitnessProvider<PlBeliefSet,PropositionalFormula> |
HsInconsistencyMeasurementProcess.witnessProvider
The witness provider used.
|
private ConsistencyWitnessProvider<PlBeliefSet,PropositionalFormula> |
ContensionInconsistencyMeasurementProcess.witnessProvider
The witness provider used.
|
Modifier and Type | Method and Description |
---|---|
static InconsistencyMeasure<BeliefSet<PropositionalFormula>> |
InconsistencyMeasureFactory.getInconsistencyMeasure(InconsistencyMeasureFactory.Measure im)
Creates a new inconsistency measure of the given type with default
settings.
|
Modifier and Type | Method and Description |
---|---|
double |
PossibleWorldDistance.distance(PropositionalFormula f,
PossibleWorld b) |
private int |
PmInconsistencyMeasure.getNumOfMinmalProofs(PropositionalFormula f,
java.util.Collection<PropositionalFormula> formulas)
Returns the number of minimal proofs of f in formulas.
|
private Term |
FuzzyInconsistencyMeasure.getTerm(PropositionalFormula formula,
java.util.Map<Proposition,Variable> assignments)
Returns a mathematical term representation of the given formula by replacing
proposition by their given mathematical variables and replacing conjunction, disjunction,
and negation by their fuzzy counterparts (taking the given t-norm and t-conorm into account).
|
protected double |
HsInconsistencyMeasurementProcess.update(PropositionalFormula formula) |
protected double |
ContensionInconsistencyMeasurementProcess.update(PropositionalFormula formula) |
Modifier and Type | Method and Description |
---|---|
private Pair<java.util.Map<Variable,Term>,java.lang.Double> |
FuzzyInconsistencyMeasure.constructAndSolveProblem(java.util.Collection<PropositionalFormula> formulas,
java.util.Map<Proposition,Variable> assignments)
Utility method
|
private int |
PmInconsistencyMeasure.getNumOfMinmalProofs(PropositionalFormula f,
java.util.Collection<PropositionalFormula> formulas)
Returns the number of minimal proofs of f in formulas.
|
FuzzyInterpretation |
FuzzyInconsistencyMeasure.getOptimalInterpretation(java.util.Collection<PropositionalFormula> formulas)
Returns an optimal interpretation as a witness for the inconsistency value.
|
java.lang.Double |
FbInconsistencyMeasure.inconsistencyMeasure(java.util.Collection<PropositionalFormula> formulas) |
java.lang.Double |
MusVarInconsistencyMeasure.inconsistencyMeasure(java.util.Collection<PropositionalFormula> formulas) |
java.lang.Double |
PmInconsistencyMeasure.inconsistencyMeasure(java.util.Collection<PropositionalFormula> formulas) |
java.lang.Double |
ContensionInconsistencyMeasure.inconsistencyMeasure(java.util.Collection<PropositionalFormula> formulas) |
java.lang.Double |
FuzzyInconsistencyMeasure.inconsistencyMeasure(java.util.Collection<PropositionalFormula> formulas) |
Modifier and Type | Method and Description |
---|---|
private PropositionalFormula |
PlParser.parseAtomic(java.util.List<java.lang.Object> l)
Parses a simple formula as a list of String tokens or formulas into a propositional formula.
|
private PropositionalFormula |
PlParser.parseConjunction(java.util.List<java.lang.Object> l)
Parses a simple formula as a list of String tokens or formulas into a propositional formula.
|
private PropositionalFormula |
PlParser.parseDisjunction(java.util.List<java.lang.Object> l)
Parses a simple formula as a list of String tokens or formulas into a propositional formula.
|
PropositionalFormula |
PlParser.parseFormula(java.io.Reader reader) |
private PropositionalFormula |
PlParser.parseNegation(java.util.List<java.lang.Object> l)
Parses a simple formula as a list of String tokens or formulas into a propositional formula.
|
Modifier and Type | Method and Description |
---|---|
boolean |
ImMonotony.isApplicable(java.util.Collection<PropositionalFormula> kb) |
boolean |
ImFreeFormulaIndependence.isApplicable(java.util.Collection<PropositionalFormula> kb) |
abstract boolean |
AbstractImPostulate.isApplicable(java.util.Collection<PropositionalFormula> kb) |
boolean |
ImMonotony.isSatisfied(java.util.Collection<PropositionalFormula> kb,
BeliefSetInconsistencyMeasure<PropositionalFormula> ev) |
boolean |
ImMonotony.isSatisfied(java.util.Collection<PropositionalFormula> kb,
BeliefSetInconsistencyMeasure<PropositionalFormula> ev) |
boolean |
ImFreeFormulaIndependence.isSatisfied(java.util.Collection<PropositionalFormula> kb,
BeliefSetInconsistencyMeasure<PropositionalFormula> ev) |
boolean |
ImFreeFormulaIndependence.isSatisfied(java.util.Collection<PropositionalFormula> kb,
BeliefSetInconsistencyMeasure<PropositionalFormula> ev) |
abstract boolean |
AbstractImPostulate.isSatisfied(java.util.Collection<PropositionalFormula> kb,
BeliefSetInconsistencyMeasure<PropositionalFormula> ev) |
abstract boolean |
AbstractImPostulate.isSatisfied(java.util.Collection<PropositionalFormula> kb,
BeliefSetInconsistencyMeasure<PropositionalFormula> ev) |
boolean |
AbstractImPostulate.isSatisfied(java.util.Collection<PropositionalFormula> kb,
PostulateEvaluatable<PropositionalFormula> ev) |
boolean |
AbstractImPostulate.isSatisfied(java.util.Collection<PropositionalFormula> kb,
PostulateEvaluatable<PropositionalFormula> ev) |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<java.util.Collection<PropositionalFormula>> |
AbstractPropositionalLogicReasoner.getKernels(java.util.Collection<PropositionalFormula> formulas,
PropositionalFormula formula) |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<java.util.Collection<PropositionalFormula>> |
AbstractPropositionalLogicReasoner.getKernels(java.util.Collection<PropositionalFormula> formulas,
PropositionalFormula formula) |
boolean |
AbstractPropositionalLogicReasoner.isEquivalent(PropositionalFormula p1,
PropositionalFormula p2)
Checks whether the two formulas are equivalent
|
abstract java.lang.Boolean |
AbstractPropositionalLogicReasoner.query(PlBeliefSet beliefbase,
PropositionalFormula formula) |
java.lang.Boolean |
NaiveReasoner.query(PlBeliefSet beliefbase,
PropositionalFormula formula) |
java.lang.Boolean |
SatReasoner.query(PlBeliefSet beliefbase,
PropositionalFormula formula) |
boolean |
AbstractPropositionalLogicReasoner.query(PropositionalFormula formula,
PropositionalFormula formula2)
Checks whether the first formula entails the second.
|
Modifier and Type | Method and Description |
---|---|
java.util.Collection<java.util.Collection<PropositionalFormula>> |
AbstractPropositionalLogicReasoner.getKernels(java.util.Collection<PropositionalFormula> formulas,
PropositionalFormula formula) |
Modifier and Type | Field and Description |
---|---|
private static AbstractMusEnumerator<PropositionalFormula> |
PlMusEnumerator.defaultEnumerator
The default MUS enumerator.
|
Modifier and Type | Method and Description |
---|---|
protected static Pair<java.lang.String,java.util.List<PropositionalFormula>> |
SatSolver.convertToDimacs(java.util.Collection<PropositionalFormula> formulas)
Converts the given set of formulas to their string representation in
Dimacs CNF.
|
protected static Pair<java.io.File,java.util.List<PropositionalFormula>> |
SatSolver.createTmpDimacsFile(java.util.Collection<PropositionalFormula> formulas)
Creates a temporary file in Dimacs format and also returns a mapping between formulas and clauses.
|
static AbstractMusEnumerator<PropositionalFormula> |
PlMusEnumerator.getDefaultEnumerator()
Returns the default MUS enumerator.
If a default MUS enumerator has been configured this enumerator
is returned by this method.
|
Interpretation<PlBeliefSet,PropositionalFormula> |
SatSolver.getWitness(BeliefSet<PropositionalFormula> bs) |
Interpretation<PlBeliefSet,PropositionalFormula> |
Sat4jSolver.getWitness(java.util.Collection<PropositionalFormula> formulas) |
Interpretation<PlBeliefSet,PropositionalFormula> |
LingelingSolver.getWitness(java.util.Collection<PropositionalFormula> formulas) |
abstract Interpretation<PlBeliefSet,PropositionalFormula> |
SatSolver.getWitness(java.util.Collection<PropositionalFormula> formulas)
If the collection of formulas is consistent this method
returns some model of it or, if it is inconsistent, null.
|
Interpretation<PlBeliefSet,PropositionalFormula> |
SimpleDpllSolver.getWitness(java.util.Collection<PropositionalFormula> formulas) |
Interpretation<PlBeliefSet,PropositionalFormula> |
SatSolver.getWitness(PropositionalFormula formula) |
abstract java.util.Collection<java.util.Collection<PropositionalFormula>> |
PlMusEnumerator.minimalInconsistentSubsets(java.util.Collection<PropositionalFormula> formulas) |
java.util.Collection<java.util.Collection<PropositionalFormula>> |
MarcoMusEnumerator.minimalInconsistentSubsets(java.util.Collection<PropositionalFormula> formulas) |
java.util.Collection<java.util.Collection<PropositionalFormula>> |
MimusMusEnumerator.minimalInconsistentSubsets(java.util.Collection<PropositionalFormula> formulas) |
Modifier and Type | Method and Description |
---|---|
Interpretation<PlBeliefSet,PropositionalFormula> |
SatSolver.getWitness(PropositionalFormula formula) |
boolean |
SatSolver.isConsistent(PropositionalFormula formula) |
Modifier and Type | Method and Description |
---|---|
protected static Pair<java.lang.String,java.util.List<PropositionalFormula>> |
SatSolver.convertToDimacs(java.util.Collection<PropositionalFormula> formulas)
Converts the given set of formulas to their string representation in
Dimacs CNF.
|
protected static java.lang.String |
SatSolver.convertToDimacs(java.util.Collection<PropositionalFormula> formulas,
java.util.List<Proposition> props)
Converts the given set of formulas to their string representation in
Dimacs CNF.
|
protected static Pair<java.io.File,java.util.List<PropositionalFormula>> |
SatSolver.createTmpDimacsFile(java.util.Collection<PropositionalFormula> formulas)
Creates a temporary file in Dimacs format and also returns a mapping between formulas and clauses.
|
protected static java.io.File |
SatSolver.createTmpDimacsFile(java.util.Collection<PropositionalFormula> formulas,
java.util.List<Proposition> props)
Creates a temporary file in Dimacs format with the given proposition2variable mapping.
|
Interpretation<PlBeliefSet,PropositionalFormula> |
SatSolver.getWitness(BeliefSet<PropositionalFormula> bs) |
Interpretation<PlBeliefSet,PropositionalFormula> |
Sat4jSolver.getWitness(java.util.Collection<PropositionalFormula> formulas) |
Interpretation<PlBeliefSet,PropositionalFormula> |
LingelingSolver.getWitness(java.util.Collection<PropositionalFormula> formulas) |
abstract Interpretation<PlBeliefSet,PropositionalFormula> |
SatSolver.getWitness(java.util.Collection<PropositionalFormula> formulas)
If the collection of formulas is consistent this method
returns some model of it or, if it is inconsistent, null.
|
Interpretation<PlBeliefSet,PropositionalFormula> |
SimpleDpllSolver.getWitness(java.util.Collection<PropositionalFormula> formulas) |
boolean |
SatSolver.isConsistent(BeliefSet<PropositionalFormula> beliefSet) |
boolean |
SatSolver.isConsistent(java.util.Collection<PropositionalFormula> formulas) |
boolean |
Sat4jSolver.isSatisfiable(java.util.Collection<PropositionalFormula> formulas) |
boolean |
LingelingSolver.isSatisfiable(java.util.Collection<PropositionalFormula> formulas) |
abstract boolean |
SatSolver.isSatisfiable(java.util.Collection<PropositionalFormula> formulas)
Checks whether the given set of formulas is satisfiable.
|
boolean |
SimpleDpllSolver.isSatisfiable(java.util.Collection<PropositionalFormula> formulas) |
abstract java.util.Collection<java.util.Collection<PropositionalFormula>> |
PlMusEnumerator.minimalInconsistentSubsets(java.util.Collection<PropositionalFormula> formulas) |
java.util.Collection<java.util.Collection<PropositionalFormula>> |
MarcoMusEnumerator.minimalInconsistentSubsets(java.util.Collection<PropositionalFormula> formulas) |
java.util.Collection<java.util.Collection<PropositionalFormula>> |
MimusMusEnumerator.minimalInconsistentSubsets(java.util.Collection<PropositionalFormula> formulas) |
static void |
PlMusEnumerator.setDefaultEnumerator(AbstractMusEnumerator<PropositionalFormula> enumerator)
Sets the default MUS enumerator.
|
Modifier and Type | Method and Description |
---|---|
PropositionalFormula |
PossibleWorld.getCompleteConjunction(PropositionalSignature sig)
Returns the complete conjunction representing this possible world wrt.
|
Modifier and Type | Method and Description |
---|---|
InterpretationIterator<PropositionalFormula,PlBeliefSet,PossibleWorld> |
PossibleWorldIterator.reset() |
InterpretationIterator<PropositionalFormula,PlBeliefSet,PossibleWorld> |
PossibleWorldIterator.reset(java.util.Collection<? extends Formula> formulas) |
InterpretationIterator<PropositionalFormula,PlBeliefSet,PossibleWorld> |
PossibleWorldIterator.reset(Signature sig) |
Modifier and Type | Method and Description |
---|---|
boolean |
NicePossibleWorld.satisfies(PropositionalFormula formula) |
boolean |
PriestWorld.satisfies(PropositionalFormula formula) |
boolean |
PossibleWorld.satisfies(PropositionalFormula formula) |
boolean |
FuzzyInterpretation.satisfies(PropositionalFormula formula) |
PriestWorld.TruthValue |
PriestWorld.satisfies3VL(PropositionalFormula formula)
Determines the 3-valued truth value of the given formula.
|
Modifier and Type | Method and Description |
---|---|
boolean |
PossibleWorld.satisfies(java.util.Collection<PropositionalFormula> formulas) |
Modifier and Type | Class and Description |
---|---|
class |
AssociativePropositionalFormula
This class captures the common functionalities of formulas with an associative
operation like conjunction, disjunction, etc.
|
class |
Conjunction
This class represents a conjunction in propositional logic.
|
class |
Contradiction
A contradictory formula.
|
class |
Disjunction
This class represents a disjunction in propositional logic.
|
class |
Negation
This class models classical negation of propositional logic.
|
class |
Proposition
This class represents a simple proposition in propositional logic.
|
class |
SpecialFormula
This class captures the common functionalities of the special
formulas tautology and contradiction.
|
class |
Tautology
A tautological formula.
|
Modifier and Type | Field and Description |
---|---|
private PropositionalFormula |
Negation.formula
The formula within this negation.
|
Modifier and Type | Field and Description |
---|---|
protected AssociativeFormulaSupport<PropositionalFormula> |
AssociativePropositionalFormula.support
The inner formulas of this formula
|
Modifier and Type | Method and Description |
---|---|
PropositionalFormula |
Disjunction.clone() |
abstract PropositionalFormula |
PropositionalFormula.clone() |
PropositionalFormula |
Negation.clone() |
PropositionalFormula |
Conjunction.collapseAssociativeFormulas() |
PropositionalFormula |
SpecialFormula.collapseAssociativeFormulas() |
PropositionalFormula |
Proposition.collapseAssociativeFormulas() |
PropositionalFormula |
Disjunction.collapseAssociativeFormulas() |
abstract PropositionalFormula |
PropositionalFormula.collapseAssociativeFormulas()
This method collapses all associative operations appearing
in this term, e.g.
|
PropositionalFormula |
Negation.collapseAssociativeFormulas() |
PropositionalFormula |
AssociativePropositionalFormula.get(int index) |
PropositionalFormula |
Negation.getFormula()
Returns the formula within this negation.
|
PropositionalFormula |
AssociativePropositionalFormula.remove(int index) |
PropositionalFormula |
Conjunction.replace(Proposition p,
PropositionalFormula f,
int i) |
PropositionalFormula |
SpecialFormula.replace(Proposition p,
PropositionalFormula f,
int i) |
PropositionalFormula |
Proposition.replace(Proposition p,
PropositionalFormula f,
int i) |
PropositionalFormula |
Disjunction.replace(Proposition p,
PropositionalFormula f,
int i) |
abstract PropositionalFormula |
PropositionalFormula.replace(Proposition p,
PropositionalFormula f,
int i)
Replaces the ith instance of the proposition p by f.
|
PropositionalFormula |
Negation.replace(Proposition p,
PropositionalFormula f,
int i) |
PropositionalFormula |
AssociativePropositionalFormula.set(int index,
PropositionalFormula element) |
PropositionalFormula |
PropositionalFormula.toBlakeCanonicalForm()
This method returns this formula in Blake canonical form.
|
PropositionalFormula |
PropositionalFormula.toDnf()
This method returns this formula in disjunctive normal form (DNF).
|
PropositionalFormula |
Conjunction.toNnf() |
PropositionalFormula |
SpecialFormula.toNnf() |
PropositionalFormula |
Proposition.toNnf() |
PropositionalFormula |
Disjunction.toNnf() |
abstract PropositionalFormula |
PropositionalFormula.toNnf()
This method returns this formula in negation normal form (NNF).
|
PropositionalFormula |
Negation.toNnf() |
PropositionalFormula |
Conjunction.trim() |
PropositionalFormula |
SpecialFormula.trim() |
PropositionalFormula |
Proposition.trim() |
PropositionalFormula |
Disjunction.trim() |
abstract PropositionalFormula |
PropositionalFormula.trim()
Removes duplicates (identical formulas) from conjunctions and disjunctions and
duplicate negations.
|
PropositionalFormula |
Negation.trim() |
Modifier and Type | Method and Description |
---|---|
java.util.List<PropositionalFormula> |
AssociativePropositionalFormula.getFormulas() |
java.util.Set<PropositionalFormula> |
SpecialFormula.getLiterals() |
java.util.Set<PropositionalFormula> |
Proposition.getLiterals() |
java.util.Set<PropositionalFormula> |
AssociativePropositionalFormula.getLiterals() |
abstract java.util.Set<PropositionalFormula> |
PropositionalFormula.getLiterals()
Returns all literals, i.e.
|
java.util.Set<PropositionalFormula> |
Negation.getLiterals() |
java.util.Collection<PropositionalFormula> |
PropositionalFormula.getPrimeImplicants()
Returns the set of prime implicants of this formula.
|
java.util.Iterator<PropositionalFormula> |
AssociativePropositionalFormula.iterator() |
java.util.ListIterator<PropositionalFormula> |
AssociativePropositionalFormula.listIterator() |
java.util.ListIterator<PropositionalFormula> |
AssociativePropositionalFormula.listIterator(int index) |
java.util.List<PropositionalFormula> |
AssociativePropositionalFormula.subList(int fromIndex,
int toIndex) |
Modifier and Type | Method and Description |
---|---|
void |
AssociativePropositionalFormula.add(int index,
PropositionalFormula element) |
boolean |
AssociativePropositionalFormula.add(PropositionalFormula f) |
boolean |
Negation.hasLowerBindingPriority(PropositionalFormula other) |
PropositionalFormula |
Conjunction.replace(Proposition p,
PropositionalFormula f,
int i) |
PropositionalFormula |
SpecialFormula.replace(Proposition p,
PropositionalFormula f,
int i) |
PropositionalFormula |
Proposition.replace(Proposition p,
PropositionalFormula f,
int i) |
PropositionalFormula |
Disjunction.replace(Proposition p,
PropositionalFormula f,
int i) |
abstract PropositionalFormula |
PropositionalFormula.replace(Proposition p,
PropositionalFormula f,
int i)
Replaces the ith instance of the proposition p by f.
|
PropositionalFormula |
Negation.replace(Proposition p,
PropositionalFormula f,
int i) |
boolean |
PropositionalFormula.resolvableWith(PropositionalFormula other)
Checks whether this formula (which must be a conjunction of literals) is
resolvable with the given formulas (which is also a conjunction of literals,
i.e.
|
Conjunction |
PropositionalFormula.resolveWith(PropositionalFormula other)
Resolves this formula with the given one (both have to be conjunctive
clauses) and returns some resolvent.
|
PropositionalFormula |
AssociativePropositionalFormula.set(int index,
PropositionalFormula element) |
Modifier and Type | Method and Description |
---|---|
boolean |
AssociativePropositionalFormula.addAll(java.util.Collection<? extends PropositionalFormula> c) |
boolean |
AssociativePropositionalFormula.addAll(int index,
java.util.Collection<? extends PropositionalFormula> c) |
static PropositionalSignature |
PropositionalSignature.getSignature(java.util.Collection<? extends PropositionalFormula> formulas)
Returns the set of atoms appearing in the given collection of formulas
|
Constructor and Description |
---|
AssociativePropositionalFormula(PropositionalFormula first,
PropositionalFormula second)
Creates a new associative formula with the two given formulae
|
Conjunction(PropositionalFormula first,
PropositionalFormula second)
Creates a new conjunction with the two given formulae
|
Disjunction(PropositionalFormula first,
PropositionalFormula second)
Creates a new disjunction with the two given formulae
|
Negation(PropositionalFormula formula)
Creates a new negation with the given formula.
|
Constructor and Description |
---|
AssociativePropositionalFormula(java.util.Collection<? extends PropositionalFormula> formulas)
Creates a new associative formula with the given inner formulas.
|
Conjunction(java.util.Collection<? extends PropositionalFormula> formulas)
Creates a new conjunction with the given inner formulas.
|
Disjunction(java.util.Collection<? extends PropositionalFormula> formulas)
Creates a new disjunction with the given inner formulas.
|
PlBeliefSet(java.util.Collection<? extends PropositionalFormula> formulas)
Creates a new knowledge base with the given
set of formulas.
|
Modifier and Type | Field and Description |
---|---|
private CspInconsistencyMeasure<PropositionalFormula> |
CspInconsistencyMeasureTest.m |
Modifier and Type | Method and Description |
---|---|
private PropositionalFormula |
RandomSampler.randomFormula()
Returns a random formula.
|
PropositionalFormula |
CnfSampler.sampleFormula()
Returns a random formula
|
PropositionalFormula |
SyntacticRandomSampler.sampleFormula(ProbabilityFunction<java.lang.Byte> prob)
Samples a single formula.
|
Modifier and Type | Method and Description |
---|---|
private java.util.List<PropositionalFormula> |
HsSampler.getCanonicalFormulas(int num,
PropositionalSignature sig)
For a signature {a1,...,an} creates num different canonical and mutually exclusive
formulas of the form a1a2a3, a1a2-a3, a1-a2a3, etc.
|
private Pair<java.util.Collection<PropositionalFormula>,java.lang.Integer> |
CanonicalIterator.parseAssociativeFormula(java.util.BitSet s,
int idx,
int numOfTerms,
PropositionalSignature sig)
Parses an associate formula from the given bitset starting at index idx, with the given number
of terms and the given signature
|
private Pair<PropositionalFormula,java.lang.Integer> |
CanonicalIterator.parseFormula(java.util.BitSet s,
int idx,
PropositionalSignature sig)
Reads the next formula of the given bitset, starting at the given index.
|
private Pair<PropositionalFormula,java.lang.Integer> |
CanonicalIterator.parseProposition(java.util.BitSet s,
int idx,
PropositionalSignature sig)
Parses a proposition in bitset s starting from idx.
|
Modifier and Type | Method and Description |
---|---|
private static java.lang.String |
CanonicalIterator.formula2String(PropositionalFormula f,
java.util.Map<Proposition,java.lang.Integer> prop)
Encodes the given formula as a bitstring.
|
Constructor and Description |
---|
PlWriter(PropositionalFormula plFormula) |
Modifier and Type | Method and Description |
---|---|
PropositionalFormula |
FOLPropTranslator.toPropositional(FolFormula folFormula) |
Modifier and Type | Method and Description |
---|---|
FolFormula |
FOLPropTranslator.toFOL(PropositionalFormula propFormula) |
Modifier and Type | Field and Description |
---|---|
(package private) BeliefSet<PropositionalFormula> |
InconsistencyMeasurementService.MeasurementCallee.beliefSet |
(package private) InconsistencyMeasure<BeliefSet<PropositionalFormula>> |
InconsistencyMeasurementService.MeasurementCallee.measure |
static AbstractMusEnumerator<PropositionalFormula> |
InconsistencyMeasurementService.musEnumerator
The MUS enumerator configured for this service.
|
Constructor and Description |
---|
MeasurementCallee(InconsistencyMeasure<BeliefSet<PropositionalFormula>> measure,
BeliefSet<PropositionalFormula> beliefSet) |
MeasurementCallee(InconsistencyMeasure<BeliefSet<PropositionalFormula>> measure,
BeliefSet<PropositionalFormula> beliefSet) |