CNFReductionResRes
gapt.proofs.reduction.CNFReductionResRes
case object CNFReductionResRes extends Reduction[HOLSequent, Set[HOLClause], ResolutionProof, ResolutionProof]
Reduces finding a resolution proof for a sequent to finding a resolution proof of a clause set.
Attributes
- Source
- manySorted.scala
- Graph
-
- Supertypes
- Self type
-
CNFReductionResRes.type
Members list
Type members
Inherited types
The names of the product elements
Attributes
- Inherited from:
- Singleton
- Source
- Mirror.scala
The mirrored *-type
Attributes
- Inherited from:
- Singleton
- Source
- Mirror.scala
Inherited and Abstract types
The name of the type
Value members
Concrete methods
Attributes
- Definition Classes
- Source
- manySorted.scala
Inherited methods
Create a new instance of type T with elements taken from product p.
Create a new instance of type T with elements taken from product p.
Attributes
- Inherited from:
- Singleton
- Source
- Mirror.scala
Attributes
- Inherited from:
- Product
Attributes
- Inherited from:
- Product
def |>[P2_ >: Set[HOLClause], P3, S2_ <: ResolutionProof, S3](other: Reduction[P2_, P3, S2_, S3]): Reduction[HOLSequent, P3, ResolutionProof, S3]
Sequentially composes reductions.
In this article