Type Members

1.  case class Flip(id: String, clause_exp: SExpression, flipped: SequentIndex, conclusion: FOLClause, t: IvyResolutionProof) extends IvyResolutionProof with Product with Serializable
2.  case class InitialClause(id: String, clause_exp: SExpression, conclusion: FOLClause) extends IvyResolutionProof with Product with Serializable
3.  case class Instantiate(id: String, clause_exp: SExpression, substitution: FOLSubstitution, conclusion: FOLClause, t: IvyResolutionProof) extends IvyResolutionProof with Product with Serializable
4.  sealed trait IvyResolutionProof extends SequentProof[FOLAtom, IvyResolutionProof]

   ** Implementation of Ivy's Resolution Calculus *** Ivy has it's own variation of resolution which only resolves over identical literals but has an instantiation rule.

   ** Implementation of Ivy's Resolution Calculus *** Ivy has it's own variation of resolution which only resolves over identical literals but has an instantiation rule. It should be possible to display the proofs in prooftool, but a translation to robinson resolution is neccessary for many applications.

5.  case class NewSymbol(id: String, clause_exp: SExpression, lit: SequentIndex, new_symbol: FOLConst, replacement_term: FOLTerm, conclusion: FOLClause, t: IvyResolutionProof) extends IvyResolutionProof with Product with Serializable
6.  case class Paramodulation(id: String, clause_exp: SExpression, position: List[Int], eq: SequentIndex, lit: SequentIndex, newLit: FOLAtom, is_demodulation: Boolean, conclusion: FOLClause, t1: IvyResolutionProof, t2: IvyResolutionProof) extends IvyResolutionProof with Product with Serializable
7.  case class Propositional(id: String, clause_exp: SExpression, conclusion: FOLClause, t: IvyResolutionProof) extends IvyResolutionProof with Product with Serializable
8.  case class Resolution(id: String, clause_exp: SExpression, lit1: SequentIndex, lit2: SequentIndex, conclusion: FOLClause, t1: IvyResolutionProof, t2: IvyResolutionProof) extends IvyResolutionProof with Product with Serializable