001: package org.mandarax.reference;
002:
003: /*
004: * Copyright (C) 1999-2004 <a href="mailto:jens.dietrich@unforgettable.com">Jens Dietrich</a>
005: *
006: * This library is free software; you can redistribute it and/or
007: * modify it under the terms of the GNU Lesser General Public
008: * License as published by the Free Software Foundation; either
009: * version 2 of the License, or (at your option) any later version.
010: *
011: * This library is distributed in the hope that it will be useful,
012: * but WITHOUT ANY WARRANTY; without even the implied warranty of
013: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
014: * Lesser General Public License for more details.
015: *
016: * You should have received a copy of the GNU Lesser General Public
017: * License along with this library; if not, write to the Free Software
018: * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
019: */
020: import java.util.*;
021: import org.mandarax.kernel.*;
022: import org.mandarax.lib.Cut;
023: import org.mandarax.util.ClauseIterator;
024:
025: /**
026: * Implementation of an inference engine returning many results.
027: * Negation and cut are supported.
028: * @author <A HREF="mailto:jens.dietrich@unforgettable.com">Jens Dietrich</A>, <A HREF="mailto:a.kozlenkov@city.ac.uk">Alexander Kozlenkov</A>
029: * @version 3.4 <7 March 05>
030: * @since 2.1
031: * Prova re-integration modifications
032: * @author <A HREF="mailto:a.kozlenkov@city.ac.uk">Alex Kozlenkov</A>
033: * @version 3.4 <7 March 05>
034: */
035: public final class ResolutionInferenceEngine4 extends
036: AbstractResolutionInferenceEngine {
037:
038: /**
039: * Constructor.
040: */
041: public ResolutionInferenceEngine4() {
042: super ();
043: }
044:
045: /**
046: * Get the feature descriptions.
047: * @return the feature descriptions
048: */
049: public InferenceEngineFeatureDescriptions getFeatureDescriptions() {
050: if (featureDescriptions == null) {
051: featureDescriptions = new InferenceEngineFeatureDescriptions() {
052: protected void initialize() {
053: super .initialize();
054: this .supported
055: .add(InferenceEngineFeatureDescriptions.LOOP_CHECKS);
056: this .supported
057: .add(InferenceEngineFeatureDescriptions.MULTIPLE_RESULTS);
058: this .supported
059: .add(InferenceEngineFeatureDescriptions.NEGATION_AS_FAILURE);
060: this .supported
061: .add(InferenceEngineFeatureDescriptions.CUT);
062: this .supported
063: .add(InferenceEngineFeatureDescriptions.DERIVATION_EVENT_LISTENERS);
064: }
065:
066: };
067: }
068: return featureDescriptions;
069: }
070:
071: /**
072: * Try to proof a goal.
073: * @return a derivation node
074: * @param goal - the goal that has to be proved
075: * @param constraintPool - a vector of constraints
076: * @param queryVariables - a list of query variables
077: * @param kb - the knowledge base used
078: * @param counter - the proof step counter
079: * @param renameVariables a variable renaming
080: * @param logEnabled - indicates whether we must log this proof step
081: * @param results - the list collecting the results
082: * @param appliedClauses - a list of all clauses applied so far (used to detect loops)
083: * @param exceptionHandlingStrategy - an integer decoding the exception handling strategy when fetching and resolving
084: * ClauseSetExceptions
085: * @param cardinalityConstraint - the cardinality constraint specifying the number of results we are looking for
086: * @param listeners the derivation listeners
087: * @param session a session object
088: * @throws InferenceException
089: */
090: private DerivationNodeImpl proof(Clause goal, List constraintPool,
091: DerivationStepCounter counter,
092: VariableRenaming renameVariables, boolean logEnabled,
093: List appliedClauses, List results, SessionImpl session)
094: throws InferenceException {
095:
096: int exceptionHandlingStrategy = session
097: .getExceptionHandlingStrategy();
098: int cardinalityConstraint = session.getCardinalityContraint();
099: org.mandarax.kernel.KnowledgeBase kb = session
100: .getKnowledgeBase();
101:
102: // make sure that the session is uptodate
103: session.update(renameVariables.getAllRenamings(),
104: constraintPool);
105:
106: // for performance reasons we want to minimize checks whether log is
107: // enabled. On the other hand, we would like to switch log on / off
108: // during a proof (e.g., to analyse a long proof). This implementation
109: // checks the respective log category every 10 steps
110: boolean logOn = (counter.count % 10 == 0) ? LOG_IE_STEP
111: .isDebugEnabled() : logEnabled;
112: DerivationNodeImpl node = new DerivationNodeImpl();
113: node.setId(counter.next());
114: // node.supportedSolution = results.size();
115: DerivationNodeImpl nextNode = null;
116:
117: if (logOn) {
118: LOG_IE_STEP.debug("PROOF STEP "
119: + String.valueOf(counter.count));
120: LOG_IE_STEP.debug("Goal : " + goal.toString());
121: }
122:
123: // check for cut
124: // System.out.println("Goal before: " + goal.toString());
125: checkCut(node, goal);
126: // System.out.println("Goal after : " + goal.toString());
127:
128: // try to remove clauses using the object semantics
129: goal = performSemanticalEvaluation(goal, session, logOn);
130:
131: if (goal == null) {
132: node.setFailed(true);
133: return node;
134: }
135:
136: // check for negation (NAF)
137: goal = proofNAFClauses(goal, kb, logOn,
138: exceptionHandlingStrategy, cardinalityConstraint);
139: if (goal == null) {
140: node.setFailed(true);
141: return node;
142: }
143:
144: if (logOn) {
145: LOG_IE_STEP.debug("Goal (semantic,NAF,CUT check done): "
146: + goal.toString());
147: }
148:
149: // check whether the max proof length has been reached
150: if (counter.count >= MAXSTEPS) {
151: if (logOn) {
152: LOG_IE_STEP
153: .debug("Maximum number of steps reached, stop here !");
154: }
155: return node;
156: }
157:
158: // if the goal is the empty clause, return success
159: if (goal.isEmpty()) {
160: if (logOn) {
161: LOG_IE_STEP.debug("Derivation successful !");
162: }
163: results.add(node);
164: // new in 3.2: notify listener
165: notifyListenersOnResult(session, logOn);
166:
167: node.setResultNode(true);
168: node.setSupported(results.size() - 1);
169: node.setFailed(false);
170: // check whether we have enough results
171: if (cardinalityConstraint != ALL) {
172: node
173: .setLastNode((results.size() >= cardinalityConstraint));
174: }
175: return node;
176: }
177: String goalPredicateName = ((Fact) goal.getNegativeLiterals()
178: .get(0)).getPredicate().getName();
179:
180: // check for the next clause to continue. Try resolution.
181: try {
182:
183: ClauseIterator e = kb.clauses(goal, null);
184: boolean useClause = true;
185: while ((nextNode == null || !nextNode.isCut())
186: && e.hasMoreClauses()
187: && (cardinalityConstraint == ALL || results.size() < cardinalityConstraint)) {
188: useClause = true;
189: Resolution r = null;
190: Clause c = null;
191: Clause workCopy = null;
192: try {
193: c = e.nextClause();
194: workCopy = renameVariables.cloneAndRenameVars(c);
195: recordCut(node.getId(), workCopy);
196: } catch (ClauseSetException x) {
197: String msg = "Exception fetching clause from iterator for "
198: + goal;
199: LOG_IE_STEP.error(msg, x);
200: // depending on the exception handling strategy we forward the exception or carry on
201: if (exceptionHandlingStrategy == BUBBLE_EXCEPTIONS)
202: throw new InferenceException(msg, x);
203: useClause = false;
204: }
205: if (useClause
206: && (r = Resolution.resolve(workCopy, goal,
207: unificationAlgorithm, selectionPolicy,
208: session)) != null) {
209: appliedClauses.add(c);
210:
211: if (loopCheckingAlgorithm
212: .isInfiniteLoop(appliedClauses)) {
213: if (logOn) {
214: LOG_IE_STEP
215: .debug("LoopChecking Algorithm "
216: + loopCheckingAlgorithm
217: + " has detected a loop! Try to continue with next clause");
218: }
219: } else {
220: // log
221: if (logOn) {
222: LOG_IE_STEP
223: .debug("Can apply the following rule:");
224: LOG_IE_STEP.debug("Clause : "
225: + c.toString());
226: LOG_IE_STEP.debug("Clause (rn): "
227: + workCopy.toString());
228:
229: // log unification
230: Replacement nextReplacement = null;
231:
232: for (Iterator er = r.unification.replacements
233: .iterator(); er.hasNext();) {
234: nextReplacement = (Replacement) er
235: .next();
236: LOG_IE_STEP.debug("unify : "
237: + nextReplacement.original
238: .toString()
239: + " -> "
240: + nextReplacement.replacement
241: .toString());
242: }
243: }
244:
245: // build a new subgoal
246: Clause nextGoal = getNextGoal(workCopy, goal, r);
247:
248: // build a new constraint pool for the next step
249: List nextConstraintPool = getNextConstraintPool(
250: constraintPool, r);
251:
252: // apply constraints
253: nextGoal = nextGoal.apply(nextConstraintPool);
254:
255: // rename variables in the subgoal
256: nextGoal = renameVariables
257: .cloneAndRenameVars(nextGoal);
258:
259: // keep the renamed var here, otherwise they get overridden in the recursion
260: Hashtable renamed = renameVariables
261: .getRecentRenamings();
262:
263: // log renamings
264: if (logOn) {
265: Object nextRenaming = null;
266:
267: for (Enumeration er = renamed.keys(); er
268: .hasMoreElements();) {
269: nextRenaming = er.nextElement();
270: LOG_IE_STEP.debug("rename : "
271: + nextRenaming.toString()
272: + " -> "
273: + renamed.get(nextRenaming)
274: .toString());
275: }
276: }
277:
278: // proof the new subgoal
279: nextNode = proof(nextGoal, nextConstraintPool,
280: counter, renameVariables, logOn,
281: appliedClauses, results, session);
282:
283: nextNode.setQuery(goal);
284: nextNode.setAppliedClause(c);
285:
286: // register the subnode
287: node.addSubNode(nextNode);
288:
289: if (nextNode.isCut() && logOn) {
290: LOG_IE_STEP
291: .debug("Cut encountered - prune derivation tree here!");
292: }
293:
294: if (!nextNode.isFailed()) {
295: // add renamings and unification
296: nextNode.varRenamings = renamed;
297: nextNode.setUnification(r.unification);
298: }
299: }
300: } else {
301: if (logOn) {
302: LOG_IE_STEP
303: .debug("Cannot apply the following rule:");
304: LOG_IE_STEP.debug("Clause : "
305: + c.toString());
306: LOG_IE_STEP.debug("Clause (rn): "
307: + workCopy.toString());
308: }
309: }
310: }
311: // release resources!
312: e.close();
313: } catch (ClauseSetException x) {
314: String msg = "Exception getting clause iterator for "
315: + goal;
316: LOG_IE_STEP.error(msg, x);
317: if (exceptionHandlingStrategy == BUBBLE_EXCEPTIONS)
318: throw new InferenceException(msg, x);
319: }
320: if ((nextNode == null) || nextNode.isFailed()) {
321: List l = node.getSubNodes();
322: int n = l.size();
323: boolean result = true;
324: for (int i = 0; i < n; i++) {
325: result = result
326: && ((DerivationNodeImpl) l.get(i)).isFailed();
327: node.setFailed(result);
328: }
329: // new in 1.9.2
330: node.setFailed(result);
331: }
332: if (node != null) {
333: boolean nextCut = (nextNode != null)
334: && nextNode.isCut()
335: && !(nextNode.getCutPredicate()
336: .equals(goalPredicateName));
337: node.setCut(node.isCut() || nextCut);
338: if (nextCut && node.isCut()) {
339: // The cut level that survived up to here from deeper calls takes precedence
340: node.setCutPredicate(nextNode.getCutPredicate());
341: }
342: }
343: return node;
344: }
345:
346: /**
347: * Try to proof prereqs. If the proof succeeds, remove them from the goal.
348: * If the proof fails, return null.
349: * @param goal a goal
350: * @param kb - the knowledge base used
351: * @param logOn - indicates whether we must log this proof step
352: * @param exceptionHandlingStrategy - an integer decoding the exception handling strategy when fetching and resolving
353: * ClauseSetExceptions
354: * @param cardinalityConstraint - the cardinality constraint specifying the number of results we are looking for
355: * @return the new goal
356: */
357: private Clause proofNAFClauses(Clause goal,
358: org.mandarax.kernel.KnowledgeBase kb, boolean logOn,
359: int exceptionHandlingStrategy, int cardinalityConstraint)
360: throws InferenceException {
361: Fact literal = null;
362: for (Iterator it = goal.getNegativeLiterals().iterator(); it
363: .hasNext();) {
364: literal = (Fact) it.next();
365: if (literal.isNegatedAF() && !IEUtils.containsVars(literal)) {
366: if (logOn)
367: LOG_IE.debug("Evaluate NAF " + literal);
368: // build new query
369: Query query = LogicFactory.getDefaultFactory()
370: .createQuery(
371: LogicFactory.getDefaultFactory()
372: .createFact(
373: literal.getPredicate(),
374: literal.getTerms()),
375: "Query to proof NAF in " + literal);
376: // issue query
377: boolean proved = false;
378: try {
379: ResultSet rs = this .query(query, kb,
380: cardinalityConstraint,
381: exceptionHandlingStrategy);
382: proved = !rs.next();
383: } catch (InferenceException x) {
384: LOG_IE_STEP.error("Error proofing NAF: " + literal,
385: x);
386: if (exceptionHandlingStrategy == BUBBLE_EXCEPTIONS)
387: throw x;
388: else {
389: // assume failure proofs NAF !
390: LOG_IE_STEP
391: .debug("Assume error means failure and verifies NAF "
392: + literal);
393: proved = true;
394: }
395: }
396: // remove if proved
397: if (proved) {
398: LOG_IE_STEP.debug("Remove from list " + literal);
399: it.remove();
400: } else {
401: LOG_IE_STEP.debug("Cannot prove " + literal
402: + " (unnegated fact is provable)");
403: return null;
404: }
405: }
406: }
407: return goal;
408: }
409:
410: /**
411: * Answer a query, retrieve (multiple different) result.
412: * The cardinality contraints describe how many results should be computed. It is either
413: * <ol>
414: * <li> <code>ONE</code> - indicating that only one answer is expected
415: * <li> <code>ALL</code> - indicating that all answers should be computed
416: * <li> <code>an integer value greater than 0 indicating that this number of results expected
417: * </ol>
418: * @see #ONE
419: * @see #ALL
420: * @return the result set of the query
421: * @param query the query clause
422: * @param kb the knowledge base used to answer the query
423: * @param aCardinalityConstraint the number of results expected
424: * @param exceptionHandlingPolicy one of the constants definied in this class (BUBBLE_EXCEPTIONS,TRY_NEXT)
425: * @throws an InferenceException
426: */
427: public ResultSet query(Query query,
428: org.mandarax.kernel.KnowledgeBase kb,
429: int aCardinalityConstraint, int exceptionHandlingPolicy)
430: throws InferenceException {
431: Clause firstGoal = getGoal(query);
432: VariableRenaming renameVariables = new VariableRenaming();
433: List resultNodes = new ArrayList();
434: SessionImpl session = new SessionImpl(kb, this , query,
435: exceptionHandlingPolicy, aCardinalityConstraint);
436: notifyListenersOnDerivationStart(session, LOG_IE_STEP
437: .isDebugEnabled());
438:
439: // proof
440: DerivationNodeImpl linResult = proof(firstGoal,
441: new ArrayList(), new DerivationStepCounter(),
442: renameVariables, LOG_IE_STEP.isDebugEnabled(),
443: new ArrayList(MAXSTEPS), resultNodes, session);
444: for (int i = 0; i < resultNodes.size(); i++)
445: ((DerivationNodeImpl) resultNodes.get(i))
446: .propagateSupportedSolutions();
447: linResult
448: .setSemanticEvaluationPolicy(getSemanticEvaluationPolicy());
449: return new ResultSetImpl2(linResult, resultNodes, firstGoal);
450: }
451:
452: /**
453: * Build the next goal, i.e., remove the unified terms, join the remaining clauses,
454: * and apply the unifications.
455: * @return the next goal
456: * @param c1 the first unified clause
457: * @param c2 the second unified clause
458: * @param u a resolution
459: */
460: protected Clause getNextGoal(Clause c1, Clause c2, Resolution r) {
461: TmpClause nextClause = new TmpClause();
462: nextClause.positiveLiterals = merge(c2.getPositiveLiterals(),
463: c1.getPositiveLiterals(), r.position2);
464: nextClause.negativeLiterals = merge2(c1.getNegativeLiterals(),
465: c2.getNegativeLiterals(), r.position1);
466: return nextClause;
467: }
468:
469: /**
470: * Merge lists (of facts), skip the element at the index "skip" in the second list.
471: * This method moves negated facts to the right. This increases the chances that all
472: * terms are "ground".
473: * @return a new list
474: * @param v1 the first list
475: * @param v2 the second list
476: * @param skip the index to be skipped in the second list
477: */
478: private List merge2(List v1, List v2, int skip) {
479: List merged = new ArrayList(v1.size() + v2.size());
480: int posCounter = 0;
481: Fact f = null;
482: for (int i = 0; i < v1.size(); i++) {
483: f = (Fact) v1.get(i);
484: if (!f.isNegatedAF()) {
485: merged.add(posCounter, f);
486: posCounter = posCounter + 1;
487: } else
488: merged.add(v1.get(i));
489: }
490: for (int i = 0; i < v2.size(); i++) {
491: if (skip != i) {
492: merged.add(v2.get(i));
493: }
494: }
495: return merged;
496: }
497:
498: /**
499: * Indicates whether a clause set is a cut.
500: * @param cs a clause set
501: * @return a boolean
502: */
503: private boolean isCut(ClauseSet cs) {
504: return cs.getKey() instanceof Cut;
505: }
506:
507: /**
508: * Check whether a goal has a cut.
509: */
510: private void checkCut(DerivationNodeImpl node, Clause goal) {
511: // the assumption is that cuts are only occuring in instances of TmpClause
512: // in the first proof step, goal is an instance of Fact (originating from the query),
513: // but then the predicate cannot be a cut anyway
514: // @todo check selection policies
515: if (goal instanceof TmpClause) {
516: List negLiterals = ((TmpClause) goal).getNegativeLiterals();
517: // There may be several cut(s) so use while below
518: while (negLiterals.size() > 0
519: && ((Clause) negLiterals.get(0)).getKey() instanceof Cut) {
520: // Now the node knows where this cut came from
521: node
522: .setCutPredicate(((Prerequisite) negLiterals
523: .get(0)).getExtra());
524: node.setCut(true);
525: negLiterals.remove(0);
526: }
527: }
528: }
529:
530: /**
531: * Check whether a goal generates a cut and record the node id
532: * in the prerequisite corresponding to this cut.
533: * @param id the id of the current node
534: * @param workCopy the clause about to be resolved that is checked here
535: * for the presence of cuts.
536: */
537: private boolean recordCut(int id, Clause workCopy) {
538: // Further corrections 28/04/03
539: boolean cut_found = false;
540: List negLiterals = workCopy.getNegativeLiterals();
541: for (ListIterator li = negLiterals.listIterator(); li.hasNext();) {
542: Fact clause = (Fact) li.next();
543: Object pred = clause.getKey();
544: if (pred instanceof Cut) {
545: // Record in the cut predicate itself what LHS it was opened from.
546: // Used in checkOut() when the cut is finally reached
547: ((Prerequisite) clause).setExtra(new Integer(id));
548: cut_found = true;
549: // There may be more than one cut in one rule, so continue
550: }
551: }
552: return cut_found;
553: }
554:
555: }
|