sjm.engine
Class Not

java.lang.Object
  |
  +--sjm.engine.Structure
        |
        +--sjm.engine.Not

public class Not

extends Structure

A Not is a structure that fails if it can prove itself against a program.

This simple behavior can have surprising results. For example:

     goodBachelor(X) :- male (X), not married(X);
     badBachelor(X) :- not married(X), male(X);
     married(jim);
     male(jeremy);
     male(jim);
 

Against this program, a query badBachelor(X) will find no bachelors. This rule negates married(X) which will bind uninstantiated X to jim every time. Thus married(X) will always be true, not married(X) will always be false, and there are no bad bachelors, which is untrue. The good rule instantiates X to a good candidate first, and the negation will prove or disprove itself for that candidate.

(A parser of the logic code given above will produce engine calls similar to the following code.)

     Program p = new Program();
     Variable x = new Variable("X");
     
     p.addAxiom(new Rule(new Structure[]{
         new Structure("goodBachelor", new Term[]{x}),
         new Structure("male",         new Term[]{x}),
         new Not      ("married",      new Term[]{x})}));
     
     p.addAxiom(new Rule(new Structure[]{
         new Structure("badBachelor",  new Term[]{x}),
         new Not      ("married",      new Term[]{x}),
         new Structure("male",         new Term[]{x})}));
     p.addAxiom(new Fact("married", "jim"));
     p.addAxiom(new Fact("male", "jeremy"));
     p.addAxiom(new Fact("male", "jim"));

     Query qGood = new Query(
         p, new Structure("goodBachelor", new Term[]{x}));
     while(qGood.canFindNextProof()) {
         System.out.println(
             "goodBachelor query finds: " + qGood.lookup("X"));
     }

     Query qBad = new Query(
         p, new Structure("badBachelor", new Term[]{x}));
     while(qBad.canFindNextProof()) {
         System.out.println(
             "badBachelor query finds: " + qBad.lookup("X"));
     }
 
 

Running this code prints out:

     goodBachelor query finds: jeremy
 

Fields inherited from class sjm.engine.Structure

emptyList, functor, terms

Constructor Summary

Not(java.lang.Object functor)
Contructs a Not from the specified object.

Not(java.lang.Object functor, Term[] terms)
Constructs a Not with the specified functor and terms.

Not(Structure s)
Constructs a Not version of the supplied structure.

Method Summary

Term	copyForProof(AxiomSource as, Scope scope) Create a ConsultingNot counterpart that can prove itself.
boolean	equals(java.lang.Object o) Returns true if the supplied object is an equivalent not structure.
java.lang.String	toString() Returns a string description of this Not.

Methods inherited from class sjm.engine.Structure

arity, canFindNextProof, eval, functorAndArityEquals, headAndTail, isList, list, list, list, listTailString, listTermsToString, terms, unify, unify, unify, variables

Methods inherited from class java.lang.Object

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

Constructor Detail

Not

public Not(java.lang.Object functor)

Contructs a Not from the specified object.

Such a Not will search a program for a fact that contains just the functor. For example, it might make sense to create a Not("demo") that would look for the fact demo to see if the program is in demo mode.

Parameters:

functor - the functor for this structure

Not

public Not(java.lang.Object functor,
           Term[] terms)

Constructs a Not with the specified functor and terms. This is the normal way to define a Not. This structure will be true if there is no possible proof of it in a program.

Parameters:

functor - the functor of the structure

terms - the terms of the structure, which may be either variables or other structures

Not

public Not(Structure s)

Constructs a Not version of the supplied structure.

Parameters:

structure - the structure to negate

Method Detail

copyForProof

public Term copyForProof(AxiomSource as,
                         Scope scope)

Create a ConsultingNot counterpart that can prove itself.

Overrides:

copyForProof in class Structure

Parameters:

AxiomSource - where to find axioms to prove against

Scope - the scope to use for variables in the ConsultingStructure

Returns:

a ConsultingNot counterpart that can prove itself

equals

public boolean equals(java.lang.Object o)

Returns true if the supplied object is an equivalent not structure.

Overrides:

equals in class Structure

Parameters:

object - the object to compare

Returns:

true, if the supplied object is a Not, and the two object's sub-structures are equal

toString

public java.lang.String toString()

Returns a string description of this Not.

Overrides:

toString in class Structure

Returns:

a string description of this Not