object TptpHOLExporter extends TptpHOLExporter

Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TptpHOLExporter
  2. TptpHOLExporter
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. type CNameMap = Map[Const, String]
    Definition Classes
    TptpHOLExporter
  2. type NameMap = Map[Var, String]
    Definition Classes
    TptpHOLExporter

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def appendPostfix(str: String, l: List[String]): FormulaRole
    Definition Classes
    TptpHOLExporter
  5. def apply(seq: ExpansionSequent, filename: String, maximize_axiom_declarations: Boolean, lambda_lifting: Boolean): Unit

    Exports an expansion proof as TPTP thf problem to prove validity

    Exports an expansion proof as TPTP thf problem to prove validity

    seq

    the sequent to export

    filename

    the filename

    maximize_axiom_declarations

    if true, all conjunctions

    lambda_lifting

    apply lambda lifting to deep formula and add the definitions into to the antecedent of the formula

    Definition Classes
    TptpHOLExporter
  6. def apply(seq: HOLSequent, filename: String, separate_axioms: Boolean = false): Unit

    Exports a sequent as TPTP thf problem to prove validity

    Exports a sequent as TPTP thf problem to prove validity

    seq

    the sequent to export

    filename

    the filename

    Definition Classes
    TptpHOLExporter
  7. def apply(ls: List[HOLSequent], filename: String): Unit

    Exports a sequent set as TPTP thf problem to prove unsatisfiability

    Exports a sequent set as TPTP thf problem to prove unsatisfiability

    ls

    the list of sequents to export

    filename

    the filename

    Definition Classes
    TptpHOLExporter
  8. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  9. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
  10. def closedFormula(fs: HOLSequent): Formula
    Definition Classes
    TptpHOLExporter
  11. def createFormula(f: Expr, map: Map[Var, String]): String
    Definition Classes
    TptpHOLExporter
  12. def createNamesFromConst(l: List[Const]): CNameMap
    Definition Classes
    TptpHOLExporter
  13. def createNamesFromSequent(l: List[HOLSequent]): (List[Var], NameMap, List[Const], CNameMap)
    Definition Classes
    TptpHOLExporter
  14. def createNamesFromVar(l: List[Var]): NameMap
    Definition Classes
    TptpHOLExporter
  15. val emptyCNameMap: Map[Const, String]
    Definition Classes
    TptpHOLExporter
  16. val emptyNameMap: Map[Var, String]
    Definition Classes
    TptpHOLExporter
  17. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  18. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  19. def export(ep: ExpansionSequent, maximize_axiom_declarations: Boolean = true, lambda_lifting: Boolean = false): String

    Exports an expansion proof as TPTP thf problem.

    Exports an expansion proof as TPTP thf problem. The antedent of the

    ep

    the expansion proof to export

    maximize_axiom_declarations

    if true, all conjunctions

    lambda_lifting

    apply lambda lifting to deep formula and add the definitions into to the antecedent of the formula

    Definition Classes
    TptpHOLExporter
  20. def export_negative(ls: List[HOLSequent]): String

    Exports a sequent set as TPTP thf problem to prove unsatisfiability

    Exports a sequent set as TPTP thf problem to prove unsatisfiability

    ls

    the list of sequents to export

    Definition Classes
    TptpHOLExporter
  21. def export_positive(seq: HOLSequent, separate_axioms: Boolean = false): String

    Exports a sequent as TPTP thf problem to prove validity

    Exports a sequent as TPTP thf problem to prove validity

    seq

    the sequent to be proved valid

    Definition Classes
    TptpHOLExporter
  22. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  23. def getConsts(t: Expr, set: Set[Const]): Set[Const]
    Definition Classes
    TptpHOLExporter
  24. def getTypeString(t: Ty, outer: Boolean): String
    Definition Classes
    TptpHOLExporter
  25. def getTypeString(t: Ty): String
    Definition Classes
    TptpHOLExporter
  26. def getVars(t: Expr, set: Set[Var]): Set[Var]

    extract all variables, bound and free

    extract all variables, bound and free

    Definition Classes
    TptpHOLExporter
  27. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  28. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  29. def lambda_lift_and_add_definitions(seq: HOLSequent): HOLSequent
    Definition Classes
    TptpHOLExporter
  30. def mkConstName(str: String, map: CNameMap): String
    Definition Classes
    TptpHOLExporter
  31. def mkVarName(str: String, map: Map[Var, String]): String
    Definition Classes
    TptpHOLExporter
  32. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  33. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  34. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  35. def printStatistics(vnames: NameMap, cnames: CNameMap): Unit
    Definition Classes
    TptpHOLExporter
  36. def simplify_antecedent(es: ExpansionSequent): ExpansionSequent
    Definition Classes
    TptpHOLExporter
  37. def simplify_antecedent2(es: HOLSequent): HOLSequent
    Definition Classes
    TptpHOLExporter
  38. def strip_lambdas(e: Expr, context: List[Var]): (Expr, List[Var])
    Definition Classes
    TptpHOLExporter
  39. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  40. def thf_formula(f: Expr, vmap: NameMap, cmap: CNameMap, outermost: Boolean = false): String
    Definition Classes
    TptpHOLExporter
  41. def thf_formula_dec(i: Int, f: Formula, role: TptpFormulaRole, vmap: NameMap, cmap: CNameMap): String
    Definition Classes
    TptpHOLExporter
  42. def thf_type_dec(i: Int, c: Const, cmap: CNameMap): String
    Definition Classes
    TptpHOLExporter
  43. def thf_type_dec(i: Int, v: Var, vmap: NameMap): String
    Definition Classes
    TptpHOLExporter
  44. def toString(): String
    Definition Classes
    AnyRef → Any
  45. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  46. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  47. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

Inherited from TptpHOLExporter

Inherited from AnyRef

Inherited from Any

Ungrouped