gapt.provers.prover9.Prover9
See theProver9 companion class
Attributes
- Companion
- class
- Source
- prover9.scala
- Graph
-
- Supertypes
-
class Prover9trait ExternalProgramtrait ResolutionProvertrait OneShotProvertrait Proverclass Objecttrait Matchableclass AnyShow all
- Self type
-
Prover9.type
Members list
Value members
Inherited methods
Attributes
- Inherited from:
- ResolutionProver
- Source
- ResolutionProver.scala
Attributes
- Inherited from:
- ResolutionProver
- Source
- ResolutionProver.scala
Attributes
- Inherited from:
- ResolutionProver
- Source
- ResolutionProver.scala
Attributes
- Inherited from:
- Prover
- Source
- provers.scala
Attributes
- Inherited from:
- Prover
- Source
- provers.scala
override def getExpansionProof(seq: HOLSequent)(implicit ctx0: Maybe[MutableContext]): Option[ExpansionProof]
Attributes
- Definition Classes
- Inherited from:
- ResolutionProver
- Source
- ResolutionProver.scala
def getExpansionProof(formula: Formula)(implicit ctx: Maybe[MutableContext]): Option[ExpansionProof]
Attributes
- Inherited from:
- Prover
- Source
- provers.scala
Attributes
- Inherited from:
- Prover
- Source
- provers.scala
def getLKProof(seq0: HOLSequent, addWeakenings: Boolean)(implicit ctx0: Maybe[MutableContext]): Option[LKProof]
Attributes
- Inherited from:
- ResolutionProver
- Source
- ResolutionProver.scala
Value parameters
- seq
-
The sequent that should be proved.
Attributes
- Returns
-
An LK-Proof of the sequent, or None if not successful.
- Definition Classes
- Inherited from:
- ResolutionProver
- Source
- ResolutionProver.scala
Value parameters
- formula
-
The formula that should be proved.
Attributes
- Returns
-
An LK-Proof of :- formula, or None if not successful.
- Inherited from:
- Prover
- Source
- provers.scala
override def getResolutionProof(cnf: Iterable[HOLClause])(implicit ctx: Maybe[MutableContext]): Option[ResolutionProof]
Attributes
- Definition Classes
- Inherited from:
- Prover9
- Source
- prover9.scala
def getResolutionProof(seq: HOLSequent)(implicit ctx0: Maybe[MutableContext]): Option[ResolutionProof]
Attributes
- Inherited from:
- ResolutionProver
- Source
- ResolutionProver.scala
def getResolutionProof(formula: Formula)(implicit ctx: Maybe[MutableContext]): Option[ResolutionProof]
Attributes
- Inherited from:
- ResolutionProver
- Source
- ResolutionProver.scala
def getResolutionProof(sequentSet: Iterable[HOLSequent])(implicit ctx0: Maybe[MutableContext], dummyImplicit1: DummyImplicit, dummyImplicit2: DummyImplicit): Option[ResolutionProof]
Attributes
- Inherited from:
- ResolutionProver
- Source
- ResolutionProver.scala
def getResolutionProof(cnf: Iterable[ResolutionProof])(implicit ctx: Maybe[MutableContext], dummyImplicit: DummyImplicit): Option[ResolutionProof]
Attributes
- Inherited from:
- ResolutionProver
- Source
- ResolutionProver.scala
Checks whether a set of clauses is unsatisfiable.
Checks whether a set of clauses is unsatisfiable.
Attributes
- Inherited from:
- Prover
- Source
- provers.scala
Checks whether a formula is unsatisfiable.
Value parameters
- seq
-
The sequent whose validity should be checked.
Attributes
- Returns
-
True if the formula is valid.
- Definition Classes
- Inherited from:
- ResolutionProver
- Source
- ResolutionProver.scala
Value parameters
- formula
-
The formula whose validity should be checked.
Attributes
- Returns
-
True if the formula is valid.
- Inherited from:
- Prover
- Source
- provers.scala
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.
- Definition Classes
- Inherited from:
- OneShotProver
- Source
- provers.scala
Attributes
- Inherited from:
- ResolutionProver
- Source
- ResolutionProver.scala
Inherited fields
Attributes
- Inherited from:
- Prover9
- Source
- prover9.scala
Attributes
- Inherited from:
- Prover9
- Source
- prover9.scala
In this article