aima.core.logic.propositional.inference

Class PLResolution

java.lang.Object

aima.core.logic.propositional.inference.PLResolution

public class PLResolution
extends java.lang.Object

Artificial Intelligence A Modern Approach (3rd Edition): page 255.

 
 function PL-RESOLUTION(KB, α) returns true or false
    inputs: KB, the knowledge base, a sentence in propositional logic
            α, the query, a sentence in propositional logic
            
    clauses ← the set of clauses in the CNF representation of KB ∧ ¬α
    new ← {}
    loop do
       for each pair of clauses Ci, Cj in clauses do
          resolvents ← PL-RESOLVE(Ci, Cj)
          if resolvents contains the empty clause then return true
          new ← new ∪ resolvents
       if new ⊆ clauses then return false
       clauses ← clauses ∪ new
 
 

Figure 7.12 A simple resolution algorithm for propositional logic. The function PL-RESOLVE returns the set of all possible clauses obtained by resolving its two inputs.

Note: Optional optimization added to implementation whereby tautological clauses can be removed during processing of the algorithm - see pg. 254 of AIMA3e:

Inspection of Figure 7.13 reveals that many resolution steps are pointless. For example, the clause B_1,1 ∨ ¬B_1,1 ∨ P_1,2 is equivalent to True ∨ P_1,2 which is equivalent to True. Deducing that True is true is not very helpful. Therefore, any clauses in which two complementary literals appear can be discarded.

Author:

Ciaran O'Reilly, Ravi Mohan, Mike Stampone

See Also:

Clause.isTautology()

Constructor Summary

Constructors

Constructor and Description
PLResolution() Default constructor, which will set the algorithm to discard tautologies by default.
PLResolution(boolean discardTautologies) Constructor.

Method Summary

Modifier and Type	Method and Description
protected void	discardTautologies(java.util.Set<Clause> clauses)
boolean	isDiscardTautologies()
boolean	plResolution(KnowledgeBase kb, Sentence alpha) PL-RESOLUTION(KB, α) A simple resolution algorithm for propositional logic.
java.util.Set<Clause>	plResolve(Clause ci, Clause cj) PL-RESOLVE(Ci, Cj) Calculate the set of all possible clauses by resolving its two inputs.
protected void	resolvePositiveWithNegative(Clause c1, Clause c2, java.util.Set<Clause> resolvents)
void	setDiscardTautologies(boolean discardTautologies) Determine whether or not the algorithm should discard tautological clauses during processing.
protected java.util.Set<Clause>	setOfClausesInTheCNFRepresentationOfKBAndNotAlpha(KnowledgeBase kb, Sentence alpha)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

PLResolution

public PLResolution()

Default constructor, which will set the algorithm to discard tautologies by default.

PLResolution

public PLResolution(boolean discardTautologies)

Constructor.

Parameters:

discardTautologies - true if the algorithm is to discard tautological clauses during processing, false otherwise.

Method Detail

plResolution

public boolean plResolution(KnowledgeBase kb,
                            Sentence alpha)

PL-RESOLUTION(KB, α)
A simple resolution algorithm for propositional logic.

Parameters:

kb - the knowledge base, a sentence in propositional logic.

alpha - the query, a sentence in propositional logic.

Returns:

true if KB |= α, false otherwise.

plResolve

public java.util.Set<Clause> plResolve(Clause ci,
                                       Clause cj)

PL-RESOLVE(C_i, C_j)
Calculate the set of all possible clauses by resolving its two inputs.

Parameters:

ci - clause 1

cj - clause 2

Returns:

the set of all possible clauses obtained by resolving its two inputs.

isDiscardTautologies

public boolean isDiscardTautologies()

Returns:

true if the algorithm will discard tautological clauses during processing.

setDiscardTautologies

public void setDiscardTautologies(boolean discardTautologies)

Determine whether or not the algorithm should discard tautological clauses during processing.

Parameters:

discardTautologies -

setOfClausesInTheCNFRepresentationOfKBAndNotAlpha

protected java.util.Set<Clause> setOfClausesInTheCNFRepresentationOfKBAndNotAlpha(KnowledgeBase kb,
                                                                                  Sentence alpha)

resolvePositiveWithNegative

protected void resolvePositiveWithNegative(Clause c1,
                                           Clause c2,
                                           java.util.Set<Clause> resolvents)

discardTautologies

protected void discardTautologies(java.util.Set<Clause> clauses)