Type Members

1.  sealed trait RefutationSketch extends SequentProof[FOLAtom, RefutationSketch]

   Intermediate data structure intendend for the proof replay in the TPTP proof import.

   Intermediate data structure intendend for the proof replay in the TPTP proof import.

   A refutation sketch is a list of clauses, where each clause is either an axiom (that occurs in the CNF of the original end-sequent) or is a first-order consequence of previous ones.

   These two cases are modelled as SketchAxiom and SketchInference.

2.  case class SketchAxiom(axiom: FOLClause) extends RefutationSketch with Product with Serializable

   Axiom in a refutation sketch.

   Axiom in a refutation sketch.

   The clause axiom occurs as a clause in the CNF of the end-sequent we're proving.

   axiom

   Clause of the CNF.

3.  case class SketchComponentElim(subProof: RefutationSketch, component: AvatarDefinition) extends RefutationSketch with Product with Serializable
4.  case class SketchComponentIntro(component: AvatarDefinition) extends RefutationSketch with Product with Serializable
5.  case class SketchInference(conclusion: FOLClause, from: Seq[RefutationSketch]) extends RefutationSketch with Product with Serializable

   Inference in a refutation sketch.

   Inference in a refutation sketch.

   The clause from should be a first-order consequence of the conclusions of from.

   This rule corresponds to a line in a TPTP proof which just indicates the previous lines from which it follows, but does not specify the precise inference rule employed.

   conclusion

   Conclusion of the inference.

   from

   Premises of the inference.

6.  case class SketchSplitCombine(splitCases: Seq[RefutationSketch]) extends RefutationSketch with Product with Serializable
7.  case class UnprovableSketchInference(inference: RefutationSketch) extends Product with Serializable