Theorem Prover (Programming help)

<3

So maybe one of you programmers can help me with this.

When I am trying to proof A ^ B |- A, B everything works. The antecedent is eliminated to A, B.

However when I am proving A, B |- A ^ B and introduce A ^ B, the program falls apart. So before introducing A ^ B into the antecedent I check if the both of the propositions of the introducing sequent exist in the antecedent or not, so in this case, they would be "A" and "B".

public void introduce(Sequent s)
    {
        if(s.inAntecedent(this.x) && s.inAntecedent(this.y))
        {
            s.addAntecedent(this);
        }
    }

s.inAntecedent(this.x) && s.inAntecedent(this.y) return false for some reason eventhough they should be returning true since A and B exist in the antecedent.

I really can't figure it out why it is doing this.

Here are the source files:

Proposition

import java.util.*;
        
public abstract class Proposition
{
    public abstract void eliminate_ant(Sequent s);
    
    public abstract void eliminate_con(Sequent s);
    
    public abstract void introduce(Sequent s);
    
    public abstract boolean equals(Object p);
}

Literal

import java.util.*;

public class Literal extends Proposition
{
    private String x;
    
    Literal(String p)
    {
        x = p;
    }
    
    public void eliminate_ant(Sequent s)
    {}
    
    public void eliminate_con(Sequent s)
    {}
    
    public void introduce(Sequent s)
    {}
    
    public boolean equals(Object p)
    {
        if(p instanceof Literal)
            return ((Literal)p).x == this.x;
        else
            return false;
    }
}

Conjunction

import java.util.*;

public class Conjunction extends Proposition
{
    private Proposition x;
    private Proposition y;
    
    Conjunction(Proposition p1, Proposition p2)
    {
        x = p1;
        y = p2;
    }
    
    public void eliminate_ant(Sequent s)
    {
        if(s.inAntecedent(this))
        {
            s.removeAntecedent(this);
            s.addAntecedent(this.x);
            s.addAntecedent(this.y);
        }
    }
    
    public void eliminate_con(Sequent s)
    {}
    
    public void introduce(Sequent s)
    {
        if(s.inAntecedent(this.x) && s.inAntecedent(this.y))
        {
            s.addAntecedent(this);
        }
    }
    
    public boolean equals(Object p)
    {
        if(p instanceof Conjunction)
            return (((Conjunction)p).x).equals(this.x) &&
                   (((Conjunction)p).y).equals(this.y);
        else
            return false;
    }
}

Sequent

import java.util.*;

public class Sequent
{
    private Set<Proposition> antecedent = new HashSet<Proposition>();
    private Set<Proposition> consequent = new HashSet<Proposition>();
    
    Sequent(){}
    
    public void addAntecedent(Proposition p)
    {
        antecedent.add(p);
    }
    
    public void addConsequent(Proposition p)
    {
        consequent.add(p);
    }
    
    public void removeAntecedent(Proposition p)
    {
        antecedent.remove(p);
    }
    
    public void removeConsequent(Proposition p)
    {
        consequent.remove(p);
    }
    
    public boolean inAntecedent(Proposition p)
    {
        return antecedent.contains(p);
    }
    
    public boolean inConsequent(Proposition p)
    {
        return consequent.contains(p);
    }
    
    public void eliminate()
    {
        Iterator<Proposition> i = antecedent.iterator();
        while(i.hasNext())
        {
            i.next().eliminate_ant(this);
        }
        
        i = consequent.iterator();
        while(i.hasNext())
        {
            i.next().eliminate_con(this);
        }
    }
    
    public void introduce(Proposition p)
    {
        p.introduce(this);
    }
    
    public boolean qed()
    {
        Iterator<Proposition> i = antecedent.iterator();
        Iterator<Proposition> j;
        Proposition temp;
        while(i.hasNext())
        {
            temp = i.next();
            j = consequent.iterator();
            while(j.hasNext())
            {
                if(temp.equals(j.next()))
                    return true;
            }
        }
        return false;
    }
}

Proof (main)

import java.util.*;

public class Proof 
{
    public static void main(String[] args) 
    {
        Sequent s = new Sequent();
        s.addAntecedent(new Literal("B"));
        s.addAntecedent(new Literal("A"));
        s.addConsequent(new Conjunction(new Literal("A"), new Literal("B")));
        s.eliminate();
        s.introduce(new Conjunction(new Literal("A"), new Literal("B")));
        if(s.qed())
            System.out.println("true");
        else
            System.out.println("false");
    }
}