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

TptpFOLExporter

gapt.formats.tptp.TptpFOLExporter
object TptpFOLExporter

Attributes

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

Members list

Value members

Concrete methods

def apply(formula: Formula): TptpFile

Attributes

Source
TptpFOLExporter.scala
def apply(sequent: HOLSequent): TptpFile

Attributes

Source
TptpFOLExporter.scala
def apply(sequentSet: Iterable[HOLSequent]): TptpFile

Attributes

Source
TptpFOLExporter.scala
def exportClause(clause: HOLClause, name: String): TptpInput

Attributes

Source
TptpFOLExporter.scala
def tptpProblem(ss: List[HOLClause]): TptpFile

convert a list of clauses to a CNF refutation problem.

convert a list of clauses to a CNF refutation problem.

Attributes

Source
TptpFOLExporter.scala
def tptpProblemNamed(ss: List[(String, HOLClause)]): TptpFile

convert a named list of clauses to a CNF refutation problem.

convert a named list of clauses to a CNF refutation problem.

Attributes

Source
TptpFOLExporter.scala
def tptpProofProblem(seq: HOLSequent): TptpFile

Convert a sequent into a tptp proof problem.

Convert a sequent into a tptp proof problem.

Attributes

Source
TptpFOLExporter.scala
Generated with