Further additions to proof

Author: ShobhitLamba

aima-csharp/aima-csharp.csproj

@@ -123,9 +123,12 @@
     <Compile Include="logic\fol\inference\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" />
     <Compile Include="logic\fol\inference\proof\ProofPrinter.cs" />
     <Compile Include="logic\fol\inference\proof\ProofStep.cs" />
     <Compile Include="logic\fol\inference\proof\ProofStepGoal.cs" />
+    <Compile Include="logic\fol\inference\proof\ProofStepPremise.cs" />
+    <Compile Include="logic\fol\inference\proof\ProofStepRenaming.cs" />
     <Compile Include="logic\fol\kb\data\Chain.cs" />
     <Compile Include="logic\fol\kb\data\Clause.cs" />
     <Compile Include="logic\fol\kb\data\CNF.cs" />

aima-csharp/logic/fol/inference/proof/ProofFinal.cs

@@ -0,0 +1,113 @@
+using System;
+using System.Collections.Generic;
+using aima.core.logic.fol.parsing.ast;
+
+namespace aima.core.logic.fol.inference.proof
+{
+    /**
+     * @author Ciaran O'Reilly
+     * 
+     */
+    public class ProofFinal : Proof
+    {
+	private Dictionary<Variable, Term> answerBindings = new Dictionary<Variable, Term>();
+	private ProofStep finalStep = null;
+	private List<ProofStep> proofSteps = null;
+
+	public ProofFinal(ProofStep finalStep, Dictionary<Variable, Term> answerBindings)
+	{
+	    this.finalStep = finalStep;
+	    this.answerBindings = answerBindings;
+	}
+
+	// START-Proof
+
+	public List<ProofStep> getSteps()
+	{
+	    // Only calculate if the proof steps are actually requested.
+	    if (null == proofSteps)
+	    {
+		calculateProofSteps();
+	    }
+	    return proofSteps;
+	}
+
+	public Dictionary<Variable, Term> getAnswerBindings()
+	{
+	    return answerBindings;
+	}
+
+	public void replaceAnswerBindings(Dictionary<Variable, Term> updatedBindings)
+	{
+	    answerBindings.Clear();
+	    answerBindings = updatedBindings;
+	}
+
+	// END-Proof
+
+	public override String ToString()
+	{
+	    return answerBindings.ToString();
+	}
+
+	
+	// PRIVATE METHODS
+	
+	private void calculateProofSteps()
+	{
+	    proofSteps = new List<ProofStep>();
+	    addToProofSteps(finalStep);
+
+	    // Move all premises to the front of the
+	    // list of steps
+	    int to = 0;
+	    for (int i = 0; i < proofSteps.Count; i++)
+	    {
+		if (proofSteps[i] is ProofStepPremise)
+		{
+		    ProofStep m = proofSteps[i];
+		    proofSteps.RemoveAt(i);
+		    proofSteps.Insert(to, m);
+		    to++;
+		}
+	    }
+
+	    // Move the Goals after the premises
+	    for (int i = 0; i < proofSteps.Count; i++)
+	    {
+		if (proofSteps[i] is ProofStepGoal)
+		{
+		    ProofStep m = proofSteps[i];
+		    proofSteps.RemoveAt(i);
+		    proofSteps.Insert(to, m);
+		    to++;
+		}
+	    }
+
+	    // Assign the step #s now that all the proof
+	    // steps have been unwound
+	    for (int i = 0; i < proofSteps.Count; i++)
+	    {
+		proofSteps[i].setStepNumber(i + 1);
+	    }
+	}
+
+	private void addToProofSteps(ProofStep step)
+	{
+	    if (!proofSteps.Contains(step))
+	    {
+		proofSteps.Insert(0, step);
+	    }
+	    else
+	    {
+		proofSteps.Remove(step);
+		proofSteps.Insert(0, step);
+	    }
+	    List<ProofStep> predecessors = step.getPredecessorSteps();
+	    for (int i = predecessors.Count - 1; i >= 0; i--)
+	    {
+		addToProofSteps(predecessors[i]);
+	    }
+	}
+    }
+}

aima-csharp/logic/fol/inference/proof/ProofStepPremise.cs

@@ -0,0 +1,42 @@
+using System;
+using System.Collections.Generic;
+using System.Collections.ObjectModel;
+using System.Linq;
+
+namespace aima.core.logic.fol.inference.proof
+{
+    /**
+     * @author Ciaran O'Reilly
+     * 
+     */
+    public class ProofStepPremise : AbstractProofStep
+    {
+	private static readonly List<ProofStep> _noPredecessors = new List<ProofStep>();
+
+	private Object proof = "";
+
+	public ProofStepPremise(Object proof)
+	{
+	    this.proof = proof;
+	}
+
+	// START-ProofStep
+		
+	public override List<ProofStep> getPredecessorSteps()
+	{
+	    return new ReadOnlyCollection<ProofStep>(_noPredecessors).ToList<ProofStep>();
+	}
+		
+	public override String getProof()
+	{
+	    return proof.ToString();
+	}
+	
+	public override String getJustification()
+	{
+	    return "Premise";
+	}
+
+	// END-ProofStep
+    }
+}

aima-csharp/logic/fol/inference/proof/ProofStepRenaming.cs

@@ -0,0 +1,42 @@
+using System;
+using System.Collections.Generic;
+using System.Collections.ObjectModel;
+using System.Linq;
+
+namespace aima.core.logic.fol.inference.proof
+{
+    /**
+     * @author Ciaran O'Reilly
+     * 
+     */
+    public class ProofStepRenaming : AbstractProofStep
+    {
+	private List<ProofStep> predecessors = new List<ProofStep>();
+	private Object proof = "";
+
+	public ProofStepRenaming(Object proof, ProofStep predecessor)
+	{
+	    this.proof = proof;
+	    this.predecessors.Add(predecessor);
+	}
+
+	// START-ProofStep
+
+	public override List<ProofStep> getPredecessorSteps()
+	{
+	    return new ReadOnlyCollection<ProofStep>(predecessors).ToList<ProofStep>();
+	}
+
+	public override String getProof()
+	{
+	    return proof.ToString();
+	}
+
+	public override String getJustification()
+	{
+	    return "Renaming of " + predecessors[0].getStepNumber();
+	}
+
+	// END-ProofStep
+    }
+}