gapt
2.19.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.provers/Prover

Prover

gapt.provers.Prover
trait Prover

A prover that is able to refute HOL sequents/formulas (or subsets of HOL, like propositional logic).

TODO: exceptions to indicate that a formula is not supported (e.g. for propositional provers).

Implementors may want to override isValid(seq) to avoid parsing proofs.

Attributes

Source
provers.scala
Graph
Supertypes
class Object
trait Matchable
class Any
Known subtypes
object prover.type
class CVC4
object CVC4.type
class SmtInterpol
object SmtInterpol.type
class Z3
object Z3.type
object prover.type
object EquationalLKProver.type
object LKProver.type
object SimpleSmtSolver.type
class LeanCoP
object LeanCoP.type
trait SATSolver
trait DrupSolver
class Glucose
object Glucose.type
class PicoSAT
object PicoSAT.type
class Sat4j
object Sat4j.type
object MiniSAT.type
object SimpProver.type
class Slakje
class VeriT
object VeriT.type
class EProver
object EProver.type
class Escargot
object Escargot.type
object NonSplittingEscargot.type
object QfUfEscargot.type
object IProver.type
class Metis
object Metis.type
class Prover9
object Prover9.type
class SPASS
object SPASS.type
class Vampire
object Vampire.type
object VampireCASC.type
Show all

Members list

Value members

Abstract methods

def getLKProof(seq: HOLSequent)(implicit ctx: Maybe[MutableContext]): Option[LKProof]

Value parameters

seq

The sequent that should be proved.

Attributes

Returns

An LK-Proof of the sequent, or None if not successful.

Source
provers.scala
def runSession[A](program: Session[A]): A

Method for running a session.

Method for running a session.

Type parameters

A

The return type of the session.

Value parameters

program

A proof session.

Attributes

Returns

The result of running the session.

Source
provers.scala

Concrete methods

def getEpsilonProof(seq: HOLSequent)(implicit ctx0: Maybe[MutableContext]): Option[EpsilonProof]

Attributes

Source
provers.scala
def getEpsilonProof(formula: Formula)(implicit ctx: Maybe[MutableContext]): Option[EpsilonProof]

Attributes

Source
provers.scala
def getExpansionProof(formula: Formula)(implicit ctx: Maybe[MutableContext]): Option[ExpansionProof]

Attributes

Source
provers.scala
def getExpansionProof(seq: HOLSequent)(implicit ctx: Maybe[MutableContext]): Option[ExpansionProof]

Attributes

Source
provers.scala
def getInterpolant(tree: Tree[Formula])(implicit ctx: Maybe[Context]): Option[Tree[Formula]]

Attributes

Source
provers.scala
def getLKProof(formula: Formula)(implicit ctx: Maybe[MutableContext]): Option[LKProof]

Value parameters

formula

The formula that should be proved.

Attributes

Returns

An LK-Proof of :- formula, or None if not successful.

Source
provers.scala
def isUnsat(formula: Formula)(implicit ctx: Maybe[Context]): Boolean

Checks whether a formula is unsatisfiable.

Checks whether a formula is unsatisfiable.

Attributes

Source
provers.scala
def isUnsat(cnf: Iterable[HOLClause])(implicit ctx: Maybe[Context]): Boolean

Checks whether a set of clauses is unsatisfiable.

Checks whether a set of clauses is unsatisfiable.

Attributes

Source
provers.scala
def isValid(formula: Formula)(implicit ctx: Maybe[Context]): Boolean

Value parameters

formula

The formula whose validity should be checked.

Attributes

Returns

True if the formula is valid.

Source
provers.scala
def isValid(seq: HOLSequent)(implicit ctx: Maybe[Context]): Boolean

Value parameters

seq

The sequent whose validity should be checked.

Attributes

Returns

True if the formula is valid.

Source
provers.scala
Generated with