Restructuring the inference directory alongwith further additions to proof

Author: ShobhitLamba

aima-csharp/aima-csharp.csproj

@@ -121,6 +121,12 @@
     <Compile Include="logic\fol\inference\defaultimpl\DefaultClauseSimplifier.cs" />
     <Compile Include="logic\fol\inference\defaultimpl\DefaultLightestClauseHeuristic.cs" />
     <Compile Include="logic\fol\inference\LightestClauseHeuristic.cs" />
+    <Compile Include="logic\fol\inference\otter\ClauseFilter.cs" />
+    <Compile Include="logic\fol\inference\otter\ClauseSimplifier.cs" />
+    <Compile Include="logic\fol\inference\otter\defaultimpl\DefaultClauseFilter.cs" />
+    <Compile Include="logic\fol\inference\otter\defaultimpl\DefaultClauseSimplifier.cs" />
+    <Compile Include="logic\fol\inference\otter\defaultimpl\DefaultLightestClauseHeuristic.cs" />
+    <Compile Include="logic\fol\inference\otter\LightestClauseHeuristic.cs" />
     <Compile Include="logic\fol\inference\proof\AbstractProofStep.cs" />
     <Compile Include="logic\fol\inference\proof\Proof.cs" />
     <Compile Include="logic\fol\inference\proof\ProofFinal.cs" />

aima-csharp/logic/fol/inference/ClauseFilter.cs renamed to aima-csharp/logic/fol/inference/otter/ClauseFilter.cs

@@ -0,0 +1,79 @@
+using System;
+using System.Collections.Generic;
+using System.Text;
+using System.Linq;
+using System.Collections.ObjectModel;
+using aima.core.logic.fol.kb.data;
+using aima.core.logic.fol.parsing.ast;
+
+namespace aima.core.logic.fol.inference.proof
+{
+    /**
+     * @author Ciaran O'Reilly
+     * 
+     */
+    public class ProofStepBwChGoal : AbstractProofStep
+    {
+	private List<ProofStep> predecessors = new List<ProofStep>();
+	private Clause toProve = null;
+	private Literal currentGoal = null;
+	private Dictionary<Variable, Term> bindings = new Dictionary<Variable, Term>();
+
+	public ProofStepBwChGoal(Clause toProve, Literal currentGoal,
+		Dictionary<Variable, Term> bindings)
+	{
+	    this.toProve = toProve;
+	    this.currentGoal = currentGoal;
+	    foreach (Variable key in bindings.Keys)
+	    {
+		this.bindings.Add(key, bindings[key]);
+	    }
+	}
+
+	public Dictionary<Variable, Term> getBindings()
+	{
+	    return bindings;
+	}
+
+	public void setPredecessor(ProofStep predecessor)
+	{
+	    predecessors.Clear();
+	    predecessors.Add(predecessor);
+	}
+
+	// START-ProofStep
+
+	public override List<ProofStep> getPredecessorSteps()
+	{
+	    return new ReadOnlyCollection<ProofStep>(predecessors).ToList<ProofStep>();
+	}
+
+	public override String getProof()
+	{
+	    StringBuilder sb = new StringBuilder();
+	    List<Literal> nLits = toProve.getNegativeLiterals();
+	    for (int i = 0; i < toProve.getNumberNegativeLiterals(); i++)
+	    {
+		sb.Append(nLits[i].getAtomicSentence());
+		if (i != (toProve.getNumberNegativeLiterals() - 1))
+		{
+		    sb.Append(" AND ");
+		}
+	    }
+	    if (toProve.getNumberNegativeLiterals() > 0)
+	    {
+		sb.Append(" => ");
+	    }
+	    sb.Append(toProve.getPositiveLiterals()[0]);
+	    return sb.ToString();
+	}
+
+	public override String getJustification()
+	{
+	    return "Current Goal " + currentGoal.getAtomicSentence().ToString()
+		    + ", " + bindings;
+	}
+
+	// END-ProofStep
+    }
+}

aima-csharp/logic/fol/inference/ClauseSimplifier.cs renamed to aima-csharp/logic/fol/inference/otter/ClauseSimplifier.cs

@@ -0,0 +1,42 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Collections.ObjectModel;
+using aima.core.logic.fol.kb.data;
+
+namespace aima.core.logic.fol.inference.proof
+{
+    /**
+     * @author Ciaran O'Reilly
+     * 
+     */
+    public class ProofStepFoChAlreadyAFact : AbstractProofStep
+    {
+	private readonly List<ProofStep> _noPredecessors = new List<ProofStep>();
+	private Literal fact = null;
+
+	public ProofStepFoChAlreadyAFact(Literal fact)
+	{
+	    this.fact = fact;
+	}
+	
+	// START-ProofStep
+
+	public override List<ProofStep> getPredecessorSteps()
+	{
+	    return new ReadOnlyCollection<ProofStep>(_noPredecessors).ToList<ProofStep>();
+	}
+
+	public override String getProof()
+	{
+	    return fact.ToString();
+	}
+
+	public override String getJustification()
+	{
+	    return "Already a known fact in the KB.";
+	}
+
+	// END-ProofStep
+    }
+}

aima-csharp/logic/fol/inference/LightestClauseHeuristic.cs renamed to aima-csharp/logic/fol/inference/otter/LightestClauseHeuristic.cs

@@ -0,0 +1,65 @@
+using System;
+using System.Collections.Generic;
+using System.Text;
+using System.Linq;
+using System.Collections.ObjectModel;
+using aima.core.logic.fol.kb.data;
+using aima.core.logic.fol.parsing.ast;
+
+namespace aima.core.logic.fol.inference.proof
+{
+    /**
+     * @author Ciaran O'Reilly
+     * 
+     */
+    public class ProofStepFoChAssertFact : AbstractProofStep
+    {	
+	private List<ProofStep> predecessors = new List<ProofStep>();
+	private Clause implication = null;
+	private Literal fact = null;
+	private Dictionary<Variable, Term> bindings = null;
+
+	public ProofStepFoChAssertFact(Clause implication, Literal fact,
+		Dictionary<Variable, Term> bindings, ProofStep predecessor)
+	{
+	    this.implication = implication;
+	    this.fact = fact;
+	    this.bindings = bindings;
+	    if (null != predecessor)
+	    {
+		predecessors.Add(predecessor);
+	    }
+	}
+
+	// START-ProofStep
+
+	public override List<ProofStep> getPredecessorSteps()
+	{
+	    return new ReadOnlyCollection<ProofStep>(predecessors).ToList<ProofStep>();
+	}
+
+	public override String getProof()
+	{
+	    StringBuilder sb = new StringBuilder();
+	    List<Literal> nLits = implication.getNegativeLiterals();
+	    for (int i = 0; i < implication.getNumberNegativeLiterals(); i++)
+	    {
+		sb.Append(nLits[i].getAtomicSentence());
+		if (i != (implication.getNumberNegativeLiterals() - 1))
+		{
+		    sb.Append(" AND ");
+		}
+	    }
+	    sb.Append(" => ");
+	    sb.Append(implication.getPositiveLiterals()[0]);
+	    return sb.ToString();
+	}
+
+	public override String getJustification()
+	{
+	    return "Assert fact " + fact.ToString() + ", " + bindings;
+	}
+	
+	// END-ProofStep	
+    }
+}