code: package com.naveensundarg.shadow.prover.core;
  
  import com.naveensundarg.shadow.prover.core.proof.Justification;
  import com.naveensundarg.shadow.prover.representations.cnf.CNFFormula;
  import com.naveensundarg.shadow.prover.representations.cnf.Clause;
  import com.naveensundarg.shadow.prover.representations.cnf.Literal;
  import com.naveensundarg.shadow.prover.representations.formula.*;
  import com.naveensundarg.shadow.prover.utils.Sets;
  
  import java.util.*;
  import java.util.stream.Collectors;
  
  import static com.naveensundarg.shadow.prover.utils.CollectionUtils.newEmptyList;
  import static com.naveensundarg.shadow.prover.utils.Sets.cartesianProduct;
  import static com.naveensundarg.shadow.prover.utils.Sets.newSet;
  
  /**
   * Created by naveensundarg on 4/10/16.
   */
  public class PropositionalResolutionProver implements Prover {
      @Override
      public Optional<Justification> prove(Set<Formula> assumptions, Formula formula) {
  
          Set<CNFFormula> formulas = assumptions.stream().
                  map(PropositionalResolutionProver::convertToCNF).
                  collect(Collectors.toSet());
  
  
          formulas.add(convertToCNF(Logic.negated(formula)));
  
          Set<Clause> clauses = formulas.stream().
                  map(CNFFormula::getClauses).
                  reduce(newSet(),Sets::union);
  
  
          while(!clauses.isEmpty()){
  
              List<List<Clause>> matchingPairs = getMatchingClauses(clauses);
  
              if(matchingPairs.isEmpty()){
                  return Optional.empty();
              }
              else{
                  boolean expanded = false;
                  for (List<Clause> pair : matchingPairs) {
  
                      Clause left = pair.get(0);
                      Clause right = pair.get(1);
                      boolean leftIsAllPositive = left.getLiterals().stream().noneMatch(Literal::isNegated);
                      boolean righIsAllPositive = right.getLiterals().stream().noneMatch(Literal::isNegated);
  
  
                      if (!leftIsAllPositive && !righIsAllPositive) {
                          continue;
                      }
                      Set<Clause> resolvands = resolve(left, right);
  
  
                      if (!resolvands.isEmpty()) {
  
                          List<Clause> resolvandsList = new ArrayList<>();
                          resolvands.forEach(resolvandsList::add);
  
                          for (Clause resolvand : resolvandsList) {
                              if (resolvand.getLiterals().isEmpty()) {
                                  return Optional.of(Justification.trivial(assumptions, formula));
                              } else {
                                  if (!clauses.contains(resolvand)) {
                                      clauses.add(resolvand);
                                      expanded = true;
                                  }
                              }
                          }
  
  
                      } else {
                          return Optional.empty();
                      }
                  }
  
                  if(!expanded){
                      return Optional.empty();
  
                  }
  
  
              }
  
          }
  
          return null;
      }
  
      public static CNFFormula convertToCNF(Formula formula){
  
          if(formula instanceof Atom){
              return new CNFFormula((Atom) formula);
          }
  
          if(formula instanceof And){
              And and = (And) formula;
  
              Set<Clause> clauses = Arrays.stream(and.getArguments()).
                      map(PropositionalResolutionProver::convertToCNF).
                      map(CNFFormula::getClauses).
                      reduce(Sets.newSet(), Sets::union);
  
             return new CNFFormula(clauses);
          }
  
          if(formula instanceof Or){
  
              Or or = (Or) formula;
  
              List<Set<Clause>> clauses = Arrays.stream(or.getArguments()).
                      map(PropositionalResolutionProver::convertToCNF).
                      map(CNFFormula::getClauses).collect(Collectors.toList());
  
  
              Set<List<Clause>> prod = cartesianProduct(clauses);
  
              return new CNFFormula(prod.stream().map(x->Clause.fromClauses(x)).collect(Collectors.toSet()));
  
  
          }
  
          if(formula instanceof Implication){
  
              Implication implication = (Implication) formula;
  
              Formula antecedent = implication.getAntecedent();
              Formula consequent = implication.getConsequent();
  
              return convertToCNF(new Or(Logic.negated(antecedent),consequent));
  
  
          }
  
          if(formula instanceof BiConditional){
  
              BiConditional biConditional = (BiConditional) formula;
  
              Formula left = biConditional.getLeft();
              Formula right = biConditional.getRight();
  
              return convertToCNF(new And(new Implication(left, right), new Implication(right, left)));
  
  
          }
          if(isLiteral(formula)){
              Literal literal;
              if(formula instanceof Atom){
  
                  literal = new Literal((Atom) formula, false);
              }
              else if(formula instanceof Not){
                  Not not = (Not) formula;
                  literal = new Literal((Atom) not.getArgument(), true);
  
              }
              else{
                  throw new AssertionError(formula);
              }
              return new CNFFormula(Sets.with(new Clause(Sets.with(literal))));
          }
  
          if(formula instanceof Not){
  
              Not not = (Not) formula;
              Formula notArg =  not.getArgument();
  
  
              if(notArg instanceof Not){
  
                  return convertToCNF(((Not)notArg).getArgument());
              }
  
              if(notArg instanceof Implication){
  
                  Implication implication = (Implication) notArg;
  
                  And and = new And(implication.getAntecedent(),
                          Logic.negated(implication.getConsequent()));
                  return convertToCNF(and);
              }
  
              if(notArg instanceof BiConditional){
  
                  BiConditional biConditional = (BiConditional) notArg;
  
                  Formula left = biConditional.getLeft();
                  Formula right = biConditional.getRight();
  
                  return convertToCNF(new Or(new And(Logic.negated(left), right), new And(Logic.negated(right), left)));
              }
              if(notArg instanceof Or){
  
                  Or or = (Or) notArg;
  
                  And and = new And(Arrays.stream(or.getArguments()).
                          map(Logic::negated).collect(Collectors.toList()));
                  return convertToCNF(and);
              }
  
              if(notArg instanceof And){
  
                  And and = (And) notArg;
  
                  Or or = new Or(Arrays.stream(and.getArguments()).
                          map(Logic::negated).collect(Collectors.toList()));
                  return convertToCNF(or);
              }
          }
  
          return null;
  
      }
  
  
      private static boolean isLiteral(Formula formula){
  
          return (formula instanceof Atom) ||
                  ((formula instanceof Not) &&
                          ((Not)  formula).getArgument() instanceof Atom);
      }
      private static boolean isDNF(Formula formula){
  
          if(formula instanceof Or){
  
              Or or = (Or) formula;
  
              return Arrays.stream(or.getArguments()).
                      allMatch(disjunct -> isLiteral(disjunct));
  
  
          } else{
              return false;
          }
  
      }
  
  
      public boolean matches(Literal literal1, Literal literal2){
  
          return  literal1.getPredicate().equals(literal2.getPredicate())
                  && (literal1.isNegated() ^ literal2.isNegated());
  
      }
  
      public List<List<Clause>> getMatchingClauses(Set<Clause> clauses){
  
          List<Set<Clause>> sets = newEmptyList();
          sets.add(clauses);
          sets.add(clauses);
  
          Set<List<Clause>> possiblePairs = cartesianProduct(sets);
  
         return possiblePairs.stream().filter(possiblePair->{
              Clause left = possiblePair.get(0);
              Clause right = possiblePair.get(1);
              Set<Clause> resolvends = resolve(left, right);
             return !resolvends.isEmpty();
          }).collect(Collectors.toList());
  
  
      }
  
      public Set<Clause> resolve(Clause clause1, Clause clause2){
  
          Set<Literal> literals1 = clause1.getLiterals();
          Set<Literal> literals2 = clause2.getLiterals();
  
          List<Set<Literal>> pairs = newEmptyList();
          pairs.add(literals2);
          pairs.add(literals1);
  
          Set<List<Literal>> pairsSet = cartesianProduct(pairs);
  
          Set<List<Literal>> matches =
  
                  pairsSet.stream().filter(pair->{
              Literal left = pair.get(0);
              Literal right = pair.get(1);
  
              return matches(left, right);
          }).collect(Collectors.toSet());
  
          return matches.stream().map(match->{
              Set<Literal> l1 = Sets.remove(literals1, match.get(0));
              Set<Literal> l2 = Sets.remove(literals2, match.get(1));
  
              Set<Literal> literals = Sets.union(l1, l2);
              return new Clause(literals);
  
          }).collect(Collectors.toSet());
  
  
      }
  
  }
  