gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.formats/gapt.formats.tptp/TptpHOLExporter

TptpHOLExporter

gapt.formats.tptp.TptpHOLExporter
See theTptpHOLExporter companion class
object TptpHOLExporter extends TptpHOLExporter

Attributes

Companion
class
Source
TptpHOLExporter.scala
Graph
Supertypes
class Object
trait Matchable
class Any
Self type

Members list

Type members

Inherited types

type CNameMap = Map[Const, String]

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
type NameMap = Map[Var, String]

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala

Value members

Inherited methods

def appendPostfix(str: String, l: List[String]): FormulaRole

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
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

Value parameters

filename

the filename

lambda_lifting

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

maximize_axiom_declarations

if true, all conjunctions

seq

the sequent to export

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def apply(seq: HOLSequent, filename: String, separate_axioms: Boolean): Unit

Exports a sequent as TPTP thf problem to prove validity

Exports a sequent as TPTP thf problem to prove validity

Value parameters

filename

the filename

seq

the sequent to export

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
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

Value parameters

filename

the filename

ls

the list of sequents to export

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def closedFormula(fs: HOLSequent): Formula

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def createFormula(f: Expr, map: Map[Var, String]): String

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def createNamesFromConst(l: List[Const]): CNameMap

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def createNamesFromVar(l: List[Var]): NameMap

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def export(ep: ExpansionSequent, maximize_axiom_declarations: Boolean, lambda_lifting: Boolean): String

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

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

Value parameters

ep

the expansion proof to export

lambda_lifting

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

maximize_axiom_declarations

if true, all conjunctions

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
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

Value parameters

ls

the list of sequents to export

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def export_positive(seq: HOLSequent, separate_axioms: Boolean): String

Exports a sequent as TPTP thf problem to prove validity

Exports a sequent as TPTP thf problem to prove validity

Value parameters

seq

the sequent to be proved valid

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def getConsts(t: Expr, set: Set[Const]): Set[Const]

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def getTypeString(t: Ty, outer: Boolean): String

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def getTypeString(t: Ty): String

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def getVars(t: Expr, set: Set[Var]): Set[Var]

extract all variables, bound and free

extract all variables, bound and free

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def mkConstName(str: String, map: CNameMap): String

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def mkVarName(str: String, map: Map[Var, String]): String

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def printStatistics(vnames: NameMap, cnames: CNameMap): Unit

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def strip_lambdas(e: Expr, context: List[Var]): (Expr, List[Var])

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def thf_formula(f: Expr, vmap: NameMap, cmap: CNameMap, outermost: Boolean): String

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def thf_formula_dec(i: Int, f: Formula, role: TptpFormulaRole, vmap: NameMap, cmap: CNameMap): String

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def thf_type_dec(i: Int, c: Const, cmap: CNameMap): String

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
def thf_type_dec(i: Int, v: Var, vmap: NameMap): String

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala

Inherited fields

val emptyCNameMap: Map[Const, String]

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
val emptyNameMap: Map[Var, String]

Attributes

Inherited from:
TptpHOLExporter
Source
TptpHOLExporter.scala
Generated with